defpred S₂[ Nat] means for X being set st X c= Seg $1 holds
ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) );
A2: S₂[ 0 ]

proof

let X be set ; :: thesis: ( X c= Seg 0 implies ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A3: X c= Seg 0 ; :: thesis: ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & 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 1 <= l & l < m & m <= len (<*> NAT) & k1 = (<*> NAT) . l & k2 = (<*> NAT) . m holds
k1 < k2 ) )
thus rng (<*> NAT) = X by A3; :: thesis: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (<*> NAT) & k1 = (<*> NAT) . l & k2 = (<*> NAT) . m holds
k1 < k2
thus for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len (<*> NAT) & k1 = (<*> NAT) . l & k2 = (<*> NAT) . m holds
k1 < k2 ; :: thesis: verum

end;

A4: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A5: for X being set st X c= Seg k holds
ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & 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= Seg (k + 1) implies ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) ) )
assume A6: X c= Seg (k + 1) ; :: thesis: ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )

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

assume not X c= Seg k ; :: thesis: ex p being FinSequence of NAT st
( rng p = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 ) )
then consider x being object such that
A7: x in X and
A8: not x in Seg k ;
x in Seg (k + 1) by A6, A7;
then reconsider n = x as Element of NAT ;
A9: n = k + 1

proof

assume A10: n <> k + 1 ; :: thesis: contradiction
A11: n <= k + 1 by A6, A7, Th1;
A12: 1 <= n by A6, A7, Th1;
n <= k by A10, A11, NAT_1:8;
hence contradiction by A8, A12; :: thesis: verum

end;

set Y = X \ {(k + 1)};
A13: X \ {(k + 1)} c= Seg k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ {(k + 1)} or x in Seg k )
assume A14: x in X \ {(k + 1)} ; :: thesis: x in Seg k
then A15: x in X ;
A16: not x in {(k + 1)} by A14, XBOOLE_0:def 5;
A17: x in Seg (k + 1) by A6, A15;
A18: x <> k + 1 by A16, TARSKI:def 1;
reconsider m = x as Element of NAT by A17;
A19: m <= k + 1 by A6, A15, Th1;
A20: 1 <= m by A6, A15, Th1;
m <= k by A18, A19, NAT_1:8;
hence x in Seg k by A20; :: thesis: verum

end;

then consider p being FinSequence of NAT such that
A21: rng p = X \ {(k + 1)} and
A22: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len p & k1 = p . l & k2 = p . m holds
k1 < k2 by A5;
consider q being FinSequence such that
A23: q = p ^ <*(k + 1)*> ;
reconsider q = q as FinSequence of NAT by A23;
A24: rng q = (rng p) \/ (rng <*(k + 1)*>) by A23, Th31
.= (X \ {(k + 1)}) \/ {(k + 1)} by A21, Th38
.= X \/ {(k + 1)} by XBOOLE_1:39
.= X by A7, A9, XBOOLE_1:12, ZFMISC_1:31 ;
for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m holds
k1 < k2

proof

let l, m, k1, k2 be Nat; :: thesis: ( 1 <= l & l < m & m <= len q & k1 = q . l & k2 = q . m implies k1 < k2 )
assume that
A25: 1 <= l and
A26: l < m and
A27: m <= len q and
A28: k1 = q . l and
A29: k2 = q . m ; :: thesis: k1 < k2
l < len (p ^ <*(k + 1)*>) by A23, A26, A27, XXREAL_0:2;
then l < (len p) + (len <*(k + 1)*>) by Th22;
then l < (len p) + 1 by Th39;
then l <= len p by NAT_1:13;
then l in Seg (len p) by A25;
then A30: l in dom p by Def3;
A31: 1 <= m by A25, A26, XXREAL_0:2;

A32: now :: thesis: ( m = len q implies k1 < k2 )

assume A33: m = len q ; :: thesis: k1 < k2
k1 = p . l by A23, A28, A30, Def7;
then k1 in X \ {(k + 1)} by A21, A30, FUNCT_1:def 3;
then A34: k1 <= k by A13, Th1;
q . m = (p ^ <*(k + 1)*>) . ((len p) + (len <*(k + 1)*>)) by A23, A33, Th22
.= (p ^ <*(k + 1)*>) . ((len p) + 1) by Th39
.= k + 1 by Th42 ;
hence k1 < k2 by A29, A34, NAT_1:13; :: thesis: verum

end;

now :: thesis: ( m <> len q implies k1 < k2 )

assume m <> len q ; :: thesis: k1 < k2
then m < len (p ^ <*(k + 1)*>) by A23, A27, XXREAL_0:1;
then m < (len p) + (len <*(k + 1)*>) by Th22;
then m < (len p) + 1 by Th39;
then A35: m <= len p by NAT_1:13;
then m in Seg (len p) by A31;
then m in dom p by Def3;
then A36: k2 = p . m by A23, A29, Def7;
k1 = p . l by A23, A28, A30, Def7;
hence k1 < k2 by A22, A25, A26, A35, A36; :: thesis: verum

end;

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

end;

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

end;

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

end;

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