take f = {} ; :: thesis: ( f is NAT * -defined & f is to-naturals )
thus dom f c= NAT * ; :: according to RELAT_1:def 18 :: thesis: f is to-naturals
thus f is to-naturals ; :: thesis: verum