defpred S₁[ Nat] means for X being set st X c= Segm $1 holds
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) );
A1: ex k being Nat st X c= Segm k by Th2;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: for X being set st X c= Segm k holds
ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) ; :: thesis: S₁[k + 1]
let X be set ; :: thesis: ( X c= Segm (k + 1) implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A4: X c= Segm (k + 1) ; :: thesis: ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )

now :: thesis: ( not X c= k implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )

set Y = X \ {k};
assume not X c= k ; :: thesis: ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
then consider x being object such that
A5: x in X and
A6: not x in Segm k ;
reconsider n = x as Element of NAT by A4, A5, Th1;
n < k + 1 by A4, A5, NAT_1:44;
then A7: n <= k by NAT_1:13;
not n < k by A6, NAT_1:44;
then A8: n = k by A7, XXREAL_0:1;
A9: X \ {k} c= Segm k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ {k} or x in Segm k )
assume A10: x in X \ {k} ; :: thesis: x in Segm k
then reconsider m = x as Element of NAT by A4, Th1;
not x in {k} by A10, XBOOLE_0:def 5;
then A12: m <> k by TARSKI:def 1;
m < k + 1 by A4, A10, NAT_1:44;
then m <= k by NAT_1:13;
then m < k by A12, XXREAL_0:1;
hence x in Segm k by NAT_1:44; :: thesis: verum

end;

then consider p being XFinSequence of NAT such that
A13: rng p = X \ {k} and
A14: for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 by A3;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
consider q being XFinSequence of NAT such that
A15: q = p ^ <%k%> ;
A16: for l, m, k1, k2 being Nat st l < m & m < len q & k1 = q . l & k2 = q . m holds
k1 < k2

proof

let l, m, k1, k2 be Nat; :: thesis: ( l < m & m < len q & k1 = q . l & k2 = q . m implies k1 < k2 )
assume that
A17: l < m and
A18: m < len q and
A19: k1 = q . l and
A20: k2 = q . m ; :: thesis: k1 < k2
m + 1 <= len q by A18, NAT_1:13;
then A21: m <= (len q) - 1 by XREAL_1:19;
then l < (len (p ^ <%k%>)) - 1 by A15, A17, XXREAL_0:2;
then l < ((len p) + (len <%k%>)) - 1 by AFINSQ_1:17;
then l < ((len p) + 1) - 1 by AFINSQ_1:34;
then A22: l in dom p by AFINSQ_1:86;
A23: m <= (len q) -' 1 by A21, XREAL_0:def 2;

A24: now :: thesis: ( m <> (len q) -' 1 implies k1 < k2 )

A25: k1 = p . l by A15, A19, A22, AFINSQ_1:def 3;
assume m <> (len q) -' 1 ; :: thesis: k1 < k2
then m < (len (p ^ <%k%>)) -' 1 by A15, A23, XXREAL_0:1;
then m < ((len p) + (len <%k%>)) -' 1 by AFINSQ_1:17;
then m < ((len p) + 1) -' 1 by AFINSQ_1:34;
then A26: m < len p by NAT_D:34;
then m in dom p by AFINSQ_1:86;
then k2 = p . m by A15, A20, AFINSQ_1:def 3;
hence k1 < k2 by A14, A17, A26, A25; :: thesis: verum

end;

now :: thesis: ( m = (len q) -' 1 implies k1 < k2 )

assume m = (len q) -' 1 ; :: thesis: k1 < k2
then A27: q . m = (p ^ <%k%>) . (((len p) + (len <%k%>)) -' 1) by A15, AFINSQ_1:17
.= (p ^ <%k%>) . (((len p) + 1) -' 1) by AFINSQ_1:34
.= (p ^ <%k%>) . (len p) by NAT_D:34
.= k by AFINSQ_1:36 ;
k1 = p . l by A15, A19, A22, AFINSQ_1:def 3;
then k1 in X \ {k} by A13, A22, FUNCT_1:def 3;
hence k1 < k2 by A9, A20, A27, NAT_1:44; :: thesis: verum

end;

hence k1 < k2 by A24; :: thesis: verum

end;

A28: {k} c= X by A5, A8, ZFMISC_1:31;
rng q = (rng p) \/ (rng <%k%>) by A15, AFINSQ_1:26
.= (X \ {k}) \/ {k} by A13, AFINSQ_1:33
.= X \/ {k} by XBOOLE_1:39
.= X by A28, XBOOLE_1:12 ;
hence ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) by A16; :: thesis: verum

end;

hence ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) by A3; :: thesis: verum

end;

A29: S₁[ 0 ]

proof

let X be set ; :: thesis: ( X c= Segm 0 implies ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A30: X c= Segm 0 ; :: thesis: ex p being XFinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st l < m & m < len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
take <%> NAT ; :: thesis: ( rng (<%> NAT) = X & ( for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2 ) )
thus rng (<%> NAT) = X by A30; :: thesis: for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2
thus for l, m, k1, k2 being Nat st l < m & m < len (<%> NAT) & k1 = (<%> NAT) . l & k2 = (<%> NAT) . m holds
k1 < k2 ; :: thesis: verum

end;

for k2 being Nat holds S₁[k2] from NAT_1:sch 2(A29, A2);
hence ex b₁ being XFinSequence of NAT st
( rng b₁ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) ) by A1; :: thesis: verum