defpred S2[ 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: S2[ 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 S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[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: S2[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
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 set such that
A7: x in X and
A8: not x in Seg k by TARSKI:def 3;
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, Th3;
A12: 1 <= n by A6, A7, Th3;
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 set ; :: 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, Th3;
A20: 1 <= m by A6, A15, Th3;
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;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
consider q being FinSequence such that
A23: q = p ^ <*(k + 1)*> ;
reconsider q = q as FinSequence of NAT by A23;
A24: {(k + 1)} c= X by A7, A9, ZFMISC_1:37;
A25: rng q = (rng p) \/ (rng <*(k + 1)*>) by A23, Th44
.= (X \ {(k + 1)}) \/ {(k + 1)} by A21, Th55
.= X \/ {(k + 1)} by XBOOLE_1:39
.= X by A24, XBOOLE_1:12 ;
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
A26: 1 <= l and
A27: l < m and
A28: m <= len q and
A29: k1 = q . l and
A30: k2 = q . m ; :: thesis: k1 < k2
l < len (p ^ <*(k + 1)*>) by A23, A27, A28, XXREAL_0:2;
then l < (len p) + (len <*(k + 1)*>) by Th35;
then l < (len p) + 1 by Th56;
then l <= len p by NAT_1:13;
then l in Seg (len p) by A26, Th3;
then A31: l in dom p by Def3;
A32: 1 <= m by A26, A27, XXREAL_0:2;
A33: now
assume A34: m = len q ; :: thesis: k1 < k2
k1 = p . l by A23, A29, A31, Def7;
then k1 in X \ {(k + 1)} by A21, A31, FUNCT_1:def 5;
then A35: k1 <= k by A13, Th3;
q . m = (p ^ <*(k + 1)*>) . ((len p) + (len <*(k + 1)*>)) by A23, A34, Th35
.= (p ^ <*(k + 1)*>) . ((len p) + 1) by Th56
.= k + 1 by Th59 ;
hence k1 < k2 by A30, A35, NAT_1:13; :: thesis: verum
end;
now
assume m <> len q ; :: thesis: k1 < k2
then m < len (p ^ <*(k + 1)*>) by A23, A28, XXREAL_0:1;
then m < (len p) + (len <*(k + 1)*>) by Th35;
then m < (len p) + 1 by Th56;
then A36: m <= len p by NAT_1:13;
then m in Seg (len p) by A32, Th3;
then m in dom p by Def3;
then A37: k2 = p . m by A23, A30, Def7;
k1 = p . l by A23, A29, A31, Def7;
hence k1 < k2 by A22, A26, A27, A36, A37; :: thesis: verum
end;
hence k1 < k2 by A33; :: 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 A25; :: 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 S2[k] from NAT_1:sch 2(A2, A4);
 hence ex b1 being FinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) ) by A1; :: thesis: verum