consider m1 being Element of NAT such that
A2: ( 0 <= m1 & P₁[F₁() . m1] ) by A1;
defpred S₁[ Nat] means P₁[F₁() . $1];
A3: ex m being Nat st S₁[m] by A2;
consider M being Nat such that
A4: ( S₁[M] & ( for n being Nat st S₁[n] holds
M <= n ) ) from NAT_1:sch 5(A3);

A5: now

let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n < m & P₁[F₁() . m] )
consider m being Element of NAT such that
A6: ( n + 1 <= m & P₁[F₁() . m] ) by A1;
take m = m; :: thesis: ( n < m & P₁[F₁() . m] )
thus ( n < m & P₁[F₁() . m] ) by A6, NAT_1:13; :: thesis: verum

end;

defpred S₂[ Nat, set , set ] means for n, m being Element of NAT st $2 = n & $3 = m holds
( n < m & P₁[F₁() . m] & ( for k being Element of NAT st n < k & P₁[F₁() . k] holds
m <= k ) );
A7: for n, x being Element of NAT ex y being Element of NAT st S₂[n,x,y]

proof

let n, x be Element of NAT ; :: thesis: ex y being Element of NAT st S₂[n,x,y]
defpred S₃[ Nat] means ( x < $1 & P₁[F₁() . $1] );
ex m being Element of NAT st S₃[m] by A5;
then A8: ex m being Nat st S₃[m] ;
consider l being Nat such that
A9: ( S₃[l] & ( for k being Nat st S₃[k] holds
l <= k ) ) from NAT_1:sch 5(A8);
take l ; :: thesis: ( l is Element of REAL & l is Element of NAT & S₂[n,x,l] )
l in NAT by ORDINAL1:def 13;
hence ( l is Element of REAL & l is Element of NAT & S₂[n,x,l] ) by A9; :: thesis: verum

end;

reconsider M' = M as Element of NAT by ORDINAL1:def 13;
consider F being Function of NAT ,NAT such that
A10: ( F . 0 = M' & ( for n being Element of NAT holds S₂[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A7);
A11: ( dom F = NAT & rng F c= NAT ) by FUNCT_2:def 1;
rng F c= REAL by XBOOLE_1:1;
then reconsider F = F as Real_Sequence by A11, RELSET_1:11;

A12: now

let n be Element of NAT ; :: thesis: F . n is Element of NAT
F . n in rng F by A11, FUNCT_1:def 5;
hence F . n is Element of NAT by A11; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: F . n < F . (n + 1)
( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A12;
hence F . n < F . (n + 1) by A10; :: thesis: verum

end;

then reconsider F = F as V35() sequence of NAT by SEQM_3:def 11;
take F ; :: thesis: ( ( for n being Element of NAT holds P₁[(F₁() * F) . n] ) & ( for n being Element of NAT st ( for r being Real st r = F₁() . n holds
P₁[r] ) holds
ex m being Element of NAT st n = F . m ) )
set q = F₁() * F;
defpred S₃[ Nat] means P₁[(F₁() * F) . $1];
A13: S₃[ 0 ] by A4, A10, FUNCT_2:21;
A14: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₃[k] implies S₃[k + 1] )
assume P₁[(F₁() * F) . k] ; :: thesis: S₃[k + 1]
S₂[k,F . k,F . (k + 1)] by A10;
then P₁[F₁() . (F . (k + 1))] ;
hence S₃[k + 1] by FUNCT_2:21; :: thesis: verum

end;

thus for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A13, A14); :: thesis: for n being Element of NAT st ( for r being Real st r = F₁() . n holds
P₁[r] ) holds
ex m being Element of NAT st n = F . m
A15: for n being Element of NAT st P₁[F₁() . n] holds
ex m being Element of NAT st F . m = n

proof

defpred S₄[ Nat] means ( P₁[F₁() . $1] & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S₄[n] ; :: thesis: contradiction
then A16: ex n being Nat st S₄[n] ;
consider M1 being Nat such that
A17: ( S₄[M1] & ( for n being Nat st S₄[n] holds
M1 <= n ) ) from NAT_1:sch 5(A16);
defpred S₅[ Nat] means ( $1 < M1 & P₁[F₁() . $1] & ex m being Element of NAT st F . m = $1 );
A18: ex n being Nat st S₅[n]

proof

take M ; :: thesis: S₅[M]
A19: M <= M1 by A4, A17;
M <> M1 by A10, A17;
hence M < M1 by A19, XXREAL_0:1; :: thesis: ( P₁[F₁() . M] & ex m being Element of NAT st F . m = M )
thus P₁[F₁() . M] by A4; :: 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;

A20: for n being Nat st S₅[n] holds
n <= M1 ;
consider X being Nat such that
A21: ( S₅[X] & ( for n being Nat st S₅[n] holds
n <= X ) ) from NAT_1:sch 6(A20, A18);
A22: for k being Element of NAT st X < k & k < M1 holds
not P₁[F₁() . k]

proof

given k being Element of NAT such that A23: ( X < k & k < M1 & P₁[F₁() . 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 ) ;

suppose ex m being Element of NAT st F . m = k ; :: thesis: contradiction

hence contradiction by A21, A23; :: thesis: verum

end;

suppose for m being Element of NAT holds F . m <> k ; :: thesis: contradiction

hence contradiction by A17, A23; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

consider m being Element of NAT such that
A24: F . m = X by A21;
A25: ( X < F . (m + 1) & P₁[F₁() . (F . (m + 1))] & ( for k being Element of NAT st X < k & P₁[F₁() . k] holds
F . (m + 1) <= k ) ) by A10, A24;
M1 in NAT by ORDINAL1:def 13;
then A26: F . (m + 1) <= M1 by A10, A17, A21, A24;

now

assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A26, XXREAL_0:1;
hence contradiction by A22, A25; :: thesis: verum

end;

hence contradiction by A17; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( ( for r being Real st r = F₁() . n holds
P₁[r] ) implies ex m being Element of NAT st n = F . m )
assume for r being Real st r = F₁() . n holds
P₁[r] ; :: thesis: ex m being Element of NAT st n = F . m
then P₁[F₁() . n] ;
then consider m being Element of NAT such that
A27: F . m = n by A15;
take m ; :: thesis: n = F . m
thus n = F . m by A27; :: thesis: verum