let f be FinSubsequence; :: thesis: f is NAT -defined
ex n being Nat st dom f c= Seg n by Def12;
hence dom f c= NAT by XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum