defpred S1[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds
( n < m & P1[F1() . m] & ( for k being Element of NAT st n < k & P1[F1() . k] holds
m <= k ) );
defpred S2[ set , set , set ] means S1[$2,$3];
defpred S3[ set ] means P1[F1() . $1];
ex m1 being Element of NAT st
( 0 <= m1 & P1[F1() . m1] ) by A1;
then A2: ex m being Nat st S3[m] ;
consider M being Nat such that
A3: ( S3[M] & ( for n being Nat st S3[n] holds
M <= n ) ) from NAT_1:sch 5(A2);
 reconsider M' = M as Element of NAT by ORDINAL1:def 13;
A4: now
let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n < m & P1[F1() . m] )
consider m being Element of NAT such that
A5: ( n + 1 <= m & P1[F1() . m] ) by A1;
take m = m; :: thesis: ( n < m & P1[F1() . m] )
thus ( n < m & P1[F1() . m] ) by A5, NAT_1:13; :: thesis: verum
end;
A6: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n, x be Element of NAT ; :: thesis: ex y being Element of NAT st S2[n,x,y]
defpred S4[ Nat] means ( x < $1 & P1[F1() . $1] );
ex m being Element of NAT st S4[m] by A4;
then A7: ex m being Nat st S4[m] ;
consider l being Nat such that
A8: ( S4[l] & ( for k being Nat st S4[k] holds
l <= k ) ) from NAT_1:sch 5(A7);
 reconsider l = l as Element of NAT by ORDINAL1:def 13;
take l ; :: thesis: S2[n,x,l]
thus S2[n,x,l] by A8; :: thesis: verum
end;
consider F being Function of NAT ,NAT such that
A9: ( F . 0 = M' & ( for n being Element of NAT holds S2[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A6);
 ( dom F = NAT & rng F c= REAL ) by FUNCT_2:def 1, XBOOLE_1:1;
then reconsider F = F as natural-valued Real_Sequence by FUNCT_2:def 1, RELSET_1:11;
for n being Element of NAT holds F . n < F . (n + 1) by A9;
then reconsider F = F as increasing sequence of NAT by SEQM_3:def 11;
A10: for n being Element of NAT st P1[F1() . n] holds
ex m being Element of NAT st F . m = n
proof
defpred S4[ set ] means ( P1[F1() . $1] & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S4[n] ; :: thesis: contradiction
then A11: ex n being Nat st S4[n] ;
consider M1 being Nat such that
A12: ( S4[M1] & ( for n being Nat st S4[n] holds
M1 <= n ) ) from NAT_1:sch 5(A11);
 defpred S5[ Nat] means ( $1 < M1 & P1[F1() . $1] & ex m being Element of NAT st F . m = $1 );
A13: ex n being Nat st S5[n]
proof
take M ; :: thesis: S5[M]
( M <= M1 & M <> M1 ) by A3, A9, A12;
hence M < M1 by XXREAL_0:1; :: thesis: ( P1[F1() . M] & ex m being Element of NAT st F . m = M )
thus P1[F1() . M] by A3; :: thesis: ex m being Element of NAT st F . m = M
take 0 ; :: thesis: F . 0 = M
thus F . 0 = M by A9; :: thesis: verum
end;
A14: for n being Nat st S5[n] holds
n <= M1 ;
consider X being Nat such that
A15: ( S5[X] & ( for n being Nat st S5[n] holds
n <= X ) ) from NAT_1:sch 6(A14, A13);
 A16: for k being Element of NAT st X < k & k < M1 holds
not P1[F1() . k]
proof
given k being Element of NAT such that A17: X < k and
A18: ( k < M1 & P1[F1() . k] ) ; :: thesis: contradiction
now
per cases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Element of NAT such that
A19: F . m = X by A15;
A20: ( X < F . (m + 1) & P1[F1() . (F . (m + 1))] ) by A9, A19;
M1 in NAT by ORDINAL1:def 13;
then A21: F . (m + 1) <= M1 by A9, A12, A15, A19;
now
assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A21, XXREAL_0:1;
hence contradiction by A16, A20; :: thesis: verum
end;
hence contradiction by A12; :: thesis: verum
end;
take q = F1() * F; :: thesis: ( q is subsequence of F1() & ( for n being Element of NAT holds P1[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F1() . n holds
P1[r] ) holds
ex m being Element of NAT st F1() . n = q . m ) )
defpred S4[ set ] means P1[q . $1];
A22: for k being Element of NAT st S4[k] holds
S4[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S4[k] implies S4[k + 1] )
assume P1[q . k] ; :: thesis: S4[k + 1]
S1[F . k,F . (k + 1)] by A9;
then P1[F1() . (F . (k + 1))] ;
hence S4[k + 1] by FUNCT_2:21; :: thesis: verum
end;
thus q is subsequence of F1() ; :: thesis: ( ( for n being Element of NAT holds P1[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F1() . n holds
P1[r] ) holds
ex m being Element of NAT st F1() . n = q . m ) )
A23: S4[ 0 ] by A3, A9, FUNCT_2:21;
thus for n being Element of NAT holds S4[n] from NAT_1:sch 1(A23, A22); :: thesis: for n being Element of NAT st ( for r being Real st r = F1() . n holds
P1[r] ) holds
ex m being Element of NAT st F1() . n = q . m
let n be Element of NAT ; :: thesis: ( ( for r being Real st r = F1() . n holds
P1[r] ) implies ex m being Element of NAT st F1() . n = q . m )
assume for r being Real st r = F1() . n holds
P1[r] ; :: thesis: ex m being Element of NAT st F1() . n = q . m
then consider m being Element of NAT such that
A24: F . m = n by A10;
take m ; :: thesis: F1() . n = q . m
thus F1() . n = q . m by A24, FUNCT_2:21; :: thesis: verum