let f be PartFunc of NAT * , NAT ; :: thesis: ( f is to-naturals & f is from-natural-fseqs )
dom f c= NAT * ;
hence ( f is to-naturals & f is from-natural-fseqs ) by Def2; :: thesis: verum