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