take f = {} ; :: thesis: ( f is from-natural-fseqs & f is to-naturals )
thus dom f c= NAT * by XBOOLE_1:2; :: according to COMPUT_1:def 2 :: thesis: f is to-naturals
thus f is to-naturals ; :: thesis: verum