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 ;

hence F = SubXFinS (F,NAT) by A1, FUNCT_2:17, A2; :: thesis: verum

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

then
id (dom F) = Sgm0 (Segm (len F))
by AFINSQ_2:def 4, A3;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;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

hence F = SubXFinS (F,NAT) by A1, FUNCT_2:17, A2; :: thesis: verum