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