thus not NatMinor f is empty by Th65; :: thesis: NatMinor f is functional
let x be set ; :: according to FRAENKEL:def 1 :: thesis: ( not x in NatMinor f or x is set )
assume x in NatMinor f ; :: thesis: x is set
hence x is Function ; :: thesis: verum