theorem funcdm (A B F: set): $ func F A B -> Dom F == A $;
isfun F /\ Dom F == A /\ Ran F C_ B -> Dom F == A
func F A B -> Dom F == A