defpred S1[ Nat, set , set ] means for n, m being Element of NAT st $2 = n & $3 = m holds
( n < m & P1[F1() . m] & ( for k being Element of NAT st n < k & P1[F1() . k] holds
m <= k ) );
defpred S2[ Nat] 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 S2[m] ;
consider M being Nat such that
A3: ( S2[M] & ( for n being Nat st S2[n] holds
M <= n ) ) from NAT_1:sch 5(A2);
 reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A4: now :: thesis: for n being Element of NAT ex m being Element of NAT st
( n < m & P1[F1() . m] )
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 and
A6: P1[F1() . m] by A1;
take m = m; :: thesis: ( n < m & P1[F1() . m] )
thus ( n < m & P1[F1() . m] ) by A5, A6, NAT_1:13; :: thesis: verum
end;
A7: for n being Nat
for x being Element of NAT ex y being Element of NAT st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S1[n,x,y]
let x be Element of NAT ; :: thesis: ex y being Element of NAT st S1[n,x,y]
defpred S3[ Nat] means ( x < $1 & P1[F1() . $1] );
ex m being Element of NAT st S3[m] by A4;
then A8: ex m being Nat st S3[m] ;
consider l being Nat such that
A9: ( S3[l] & ( for k being Nat st S3[k] holds
l <= k ) ) from NAT_1:sch 5(A8);
 take l ; :: thesis: ( l is Element of NAT & S1[n,x,l] )
l in NAT by ORDINAL1:def 12;
hence ( l is Element of NAT & S1[n,x,l] ) by A9; :: thesis: verum
end;
consider F being sequence of NAT such that
A10: ( F . 0 = M9 & ( for n being Nat holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A7);
 A11: rng F c= REAL by NUMBERS:19;
A12: rng F c= NAT ;
A13: dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A11, RELSET_1:4;
A14: now :: thesis: for n being Element of NAT holds F . n is Element of NAT
let n be Element of NAT ; :: thesis: F . n is Element of NAT
F . n in rng F by A13, FUNCT_1:def 3;
hence F . n is Element of NAT by A12; :: thesis: verum
end;
now :: thesis: for n being Nat holds F . n < F . (n + 1)
let n be Nat; :: thesis: F . n < F . (n + 1)
A15: n in NAT by ORDINAL1:def 12;
A16: F . (n + 1) is Element of NAT by A14;
F . n is Element of NAT by A14, A15;
hence F . n < F . (n + 1) by A10, A16; :: thesis: verum
end;
then reconsider F = F as V43() sequence of NAT by SEQM_3:def 6;
A17: for n being Element of NAT st P1[F1() . n] holds
ex m being Element of NAT st F . m = n
proof
defpred S3[ Nat] means ( P1[F1() . $1] & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S3[n] ; :: thesis: contradiction
then A18: ex n being Nat st S3[n] ;
consider M1 being Nat such that
A19: ( S3[M1] & ( for n being Nat st S3[n] holds
M1 <= n ) ) from NAT_1:sch 5(A18);
 defpred S4[ Nat] means ( $1 < M1 & P1[F1() . $1] & ex m being Element of NAT st F . m = $1 );
A20: ex n being Nat st S4[n]
proof
take M ; :: thesis: S4[M]
A21: M <> M1 by A10, A19;
M <= M1 by A3, A19;
hence M < M1 by A21, 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 A10; :: thesis: verum
end;
A22: for n being Nat st S4[n] holds
n <= M1 ;
consider X being Nat such that
A23: ( S4[X] & ( for n being Nat st S4[n] holds
n <= X ) ) from NAT_1:sch 6(A22, A20);
 A24: 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 A25: X < k and
A26: k < M1 and
A27: P1[F1() . k] ; :: thesis: contradiction
now :: thesis: contradiction
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
A28: F . m = X by A23;
M1 in NAT by ORDINAL1:def 12;
then A29: F . (m + 1) <= M1 by A10, A19, A23, A28;
A30: P1[F1() . (F . (m + 1))] by A10, A28;
A31: X < F . (m + 1) by A10, A28;
now :: thesis: not F . (m + 1) <> M1
assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A29, XXREAL_0:1;
hence contradiction by A24, A31, A30; :: thesis: verum
end;
hence contradiction by A19; :: thesis: verum
end;
take F ; :: thesis: ( ( for n being Nat holds P1[(F1() * F) . 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 n = F . m ) )
set q = F1() * F;
defpred S3[ Nat] means P1[(F1() * F) . $1];
A32: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume P1[(F1() * F) . k] ; :: thesis: S3[k + 1]
S1[k,F . k,F . (k + 1)] by A10;
then P1[F1() . (F . (k + 1))] ;
hence S3[k + 1] by FUNCT_2:15; :: thesis: verum
end;
A33: S3[ 0 ] by A3, A10, FUNCT_2:15;
thus for n being Nat holds S3[n] from NAT_1:sch 2(A33, A32); :: 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 n = F . 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 n = F . m )
assume for r being Real st r = F1() . n holds
P1[r] ; :: thesis: ex m being Element of NAT st n = F . m
then consider m being Element of NAT such that
A34: F . m = n by A17;
take m ; :: thesis: n = F . m
thus n = F . m by A34; :: thesis: verum