defpred S₁[ Nat] means for X being set st X c= $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= 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= 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= 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= 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

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 set such that
A5: x in X and
A6: not x in k by TARSKI:def 3;
reconsider n = x as Element of NAT by A4, A5, Th1;
n < k + 1 by A4, A5, NAT_1:45;
then A7: n <= k by NAT_1:13;
not n < k by A6, NAT_1:45;
then A8: n = k by A7, XXREAL_0:1;
A9: X \ {k} c= k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ {k} or x in k )
assume A10: x in X \ {k} ; :: thesis: x in k
then A11: x in X ;
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, A11, NAT_1:45;
then m <= k by NAT_1:13;
then m < k by A12, XXREAL_0:1;
hence x in k by NAT_1:45; :: 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 13;
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:21;
then l < (len (p ^ <%k%>)) - 1 by A15, A17, XXREAL_0:2;
then l < ((len p) + (len <%k%>)) - 1 by AFINSQ_1:20;
then l < ((len p) + 1) - 1 by AFINSQ_1:38;
then A22: l in dom p by NAT_1:45;
A23: m <= (len q) -' 1 by A21, XREAL_0:def 2;

A24: now

A25: k1 = p . l by A15, A19, A22, AFINSQ_1:def 4;
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:20;
then m < ((len p) + 1) -' 1 by AFINSQ_1:38;
then A26: m < len p by NAT_D:34;
then m in dom p by NAT_1:45;
then k2 = p . m by A15, A20, AFINSQ_1:def 4;
hence k1 < k2 by A14, A17, A26, A25; :: thesis: verum

end;

now

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

end;

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

end;

A28: {k} c= X by A5, A8, ZFMISC_1:37;
rng q = (rng p) \/ (rng <%k%>) by A15, AFINSQ_1:29
.= (X \ {k}) \/ {k} by A13, AFINSQ_1:36
.= 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= 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= 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