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