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