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 n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) );
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 n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) ) )
assume A3: X c= Seg 0 ; :: thesis: ex p being FinSequence of NAT st
( rng p = X & ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) )
take <*> NAT ; :: thesis: ( rng (<*> NAT) = X & ( for n, m being Nat st 1 <= n & n < m & m <= len (<*> NAT) holds
(<*> NAT) . n < (<*> NAT) . m ) )
thus rng (<*> NAT) = X by A3; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len (<*> NAT) holds
(<*> NAT) . n < (<*> NAT) . m
thus for n, m being Nat st 1 <= n & n < m & m <= len (<*> NAT) holds
(<*> NAT) . n < (<*> NAT) . m ; :: 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 n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) ) ; :: 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 n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) ) )
assume A6: X c= Seg (k + 1) ; :: thesis: ex p being FinSequence of NAT st
( rng p = X & ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) )

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

assume not X c= Seg k ; :: thesis: ex p being FinSequence of NAT st
( rng p = X & ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) )
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, A14;
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 n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m 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 n, m being Nat st 1 <= n & n < m & m <= len q holds
q . n < q . m

proof

let l, m be Nat; :: thesis: ( 1 <= l & l < m & m <= len q implies q . l < q . m )
assume that
A25: 1 <= l and
A26: l < m and
A27: m <= len q ; :: thesis: q . l < q . m
set k2 = q . m;
set k1 = q . l;
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 q . l < q . m )

assume A33: m = len q ; :: thesis: q . l < q . m
q . l = p . l by A23, A30, Def7;
then q . l in X \ {(k + 1)} by A21, A30, FUNCT_1:def 3;
then A34: q . l <= 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 q . l < q . m by A34, NAT_1:13; :: thesis: verum

end;

now :: thesis: ( m <> len q implies q . l < q . m )

assume m <> len q ; :: thesis: q . l < q . m
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: q . m = p . m by A23, Def7;
q . l = p . l by A23, A30, Def7;
hence q . l < q . m by A22, A25, A26, A35, A36; :: thesis: verum

end;

hence q . l < q . m by A32; :: thesis: verum

end;

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

end;

hence ex p being FinSequence of NAT st
( rng p = X & ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n < p . m ) ) 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 m, n being Nat st 1 <= m & m < n & n <= len b₁ holds
b₁ . m < b₁ . n ) ) by A1; :: thesis: verum