theorem Arrowrn (A B: set) (f: nat): $ f e. Arrow A B -> Ran f C_ B $;
f e. Arrow A B <-> func f A B
func f A B -> Ran f C_ B
f e. Arrow A B -> Ran f C_ B