let F be XFinSequence; :: thesis: F = SubXFinS (F,NAT)
set SFN = Sgm0 ((len F) /\ NAT);
dom F c= NAT ;
then A1: (len F) /\ NAT = len F by XBOOLE_1:28;
A2: F is Function of (dom F),(rng F) by FUNCT_2:1;
rng (id (dom F)) c= NAT ;
then reconsider idF = id (dom F) as XFinSequence of NAT by RELAT_1:def 19;
A3: rng idF = len F ;
now :: thesis: for l, m, k1, k2 being Nat st l < m & m < len idF & k1 = idF . l & k2 = idF . m holds
k1 < k2
let l, m, k1, k2 be Nat; :: thesis: ( l < m & m < len idF & k1 = idF . l & k2 = idF . m implies k1 < k2 )
assume A4: ( l < m & m < len idF & k1 = idF . l & k2 = idF . m ) ; :: thesis: k1 < k2
then l < len idF by XXREAL_0:2;
then ( k1 = l & k2 = m ) by A4, FUNCT_1:18, AFINSQ_1:66;
hence k1 < k2 by A4; :: thesis: verum
end;
then id (dom F) = Sgm0 (Segm (len F)) by AFINSQ_2:def 4, A3;
hence F = SubXFinS (F,NAT) by A1, FUNCT_2:17, A2; :: thesis: verum