consider k being Nat such that
A6: X c= k by AE221f;
defpred S₁[ Nat] means for X being set st X c= $1 holds
ex p being XFinSequence of 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 ) );
A2: S₁[ 0 ]

proof

let X be set ; :: thesis: ( X c= 0 implies ex p being XFinSequence of 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 A3: X c= 0 ; :: thesis: ex p being XFinSequence of 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 A3; :: 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;

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= k holds
ex p being XFinSequence of 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 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 A6: X c= k + 1 ; :: thesis: ex p being XFinSequence of 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

assume not X c= k ; :: thesis: ex p being XFinSequence of 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
A7: ( x in X & not x in k ) by TARSKI:def 3;
reconsider n = x as Element of NAT by AB470, A6, A7;
n < k + 1 by A6, A7, NAT_1:45;
then A19: n <= k by NAT_1:13;
not n < k by A7, NAT_1:45;
then A8: n = k by A19, XXREAL_0:1;
set Y = X \ {k};
A10: 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 x in X \ {k} ; :: thesis: x in k
then A12n: ( x in X & not x in {k} ) by XBOOLE_0:def 5;
then reconsider m = x as Element of NAT by AB470, A6;
( m < k + 1 & m <> k ) by A12n, A6, NAT_1:45, TARSKI:def 1;
then ( m <= k & m <> k ) by NAT_1:13;
then m < k by XXREAL_0:1;
hence x in k by NAT_1:45; :: thesis: verum

end;

then consider p being XFinSequence of such that
A13: ( rng p = X \ {k} & ( for l, m, k1, k2 being Nat st 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 XFinSequence of such that
A14: q = p ^ <%k%> ;
A15: {k} c= X by A7, A8, ZFMISC_1:37;
A16: rng q = (rng p) \/ (rng <%k%>) by A14, AFINSQ_1:29
.= (X \ {k}) \/ {k} by A13, AFINSQ_1:36
.= X \/ {k} by XBOOLE_1:39
.= X by A15, XBOOLE_1:12 ;
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 A17: ( l < m & m < len q & k1 = q . l & k2 = q . m ) ; :: thesis: k1 < k2
then m + 1 <= len q by NAT_1:13;
then A38: m <= (len q) - 1 by XREAL_1:21;
A38b: m <= (len q) -' 1 by A38, XREAL_0:def 2;
A18: l in dom p

proof

l < (len (p ^ <%k%>)) - 1 by A38, A14, 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;
hence l in dom p by NAT_1:45; :: thesis: verum

end;

A20: now

assume A21: m = (len q) -' 1 ; :: thesis: k1 < k2
k1 = p . l by A14, A17, A18, AFINSQ_1:def 4;
then A22n: k1 in X \ {k} by A13, A18, FUNCT_1:def 5;
q . m = (p ^ <%k%>) . (((len p) + (len <%k%>)) -' 1) by A14, A21, 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 ;
hence k1 < k2 by A17, A10, A22n, NAT_1:45; :: thesis: verum

end;

now

assume m <> (len q) -' 1 ; :: thesis: k1 < k2
then m < (len (p ^ <%k%>)) -' 1 by A38b, A14, 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 A23: m < len p by NAT_D:34;
then m in dom p by NAT_1:45;
then A24: k2 = p . m by A14, A17, AFINSQ_1:def 4;
k1 = p . l by A14, A17, A18, AFINSQ_1:def 4;
hence k1 < k2 by A13, A17, A23, A24; :: thesis: verum

end;

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

end;

hence ex p being XFinSequence of 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 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 A5; :: thesis: verum

end;

for k2 being Nat holds S₁[k2] from NAT_1:sch 2(A2, A4);
hence ex b₁ being XFinSequence of 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 A6; :: thesis: verum