theorem Arrowisf (A B: set) (f: nat): $ f e. Arrow A B -> isfun f $;
f e. Arrow A B <-> func f A B
func f A B -> isfun f
f e. Arrow A B -> isfun f