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