theorem Arrowdm (A B: set) (f: nat): $ f e. Arrow A B -> Dom f == A $;
f e. Arrow A B <-> func f A B
func f A B -> Dom f == A
f e. Arrow A B -> Dom f == A