let s be sequence ; :: thesis: s is NAT -defined
dom s = NAT by ds;
hence s is NAT -defined by RELAT_1:def 18; :: thesis: verum