defpred S_{1}[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds

( n < m & P_{1}[F_{1}() . m] & ( for k being Element of NAT st n < k & P_{1}[F_{1}() . k] holds

m <= k ) );

defpred S_{2}[ set , set , set ] means S_{1}[$2,$3];

defpred S_{3}[ set ] means P_{1}[F_{1}() . $1];

ex m1 being Element of NAT st

( 0 <= m1 & P_{1}[F_{1}() . m1] )
by A1;

then A2: ex m being Nat st S_{3}[m]
;

consider M being Nat such that

A3: ( S_{3}[M] & ( for n being Nat st S_{3}[n] holds

M <= n ) ) from NAT_1:sch 5(A2);

reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

for x being Element of NAT ex y being Element of NAT st S_{2}[n,x,y]

A9: ( F . 0 = M9 & ( for n being Nat holds S_{2}[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A6);

( dom F = NAT & rng F c= REAL ) by FUNCT_2:def 1, NUMBERS:19;

then reconsider F = F as natural-valued Real_Sequence by FUNCT_2:def 1, RELSET_1:4;

for n being Nat holds F . n < F . (n + 1) by A9;

then reconsider F = F as increasing sequence of NAT by SEQM_3:def 6;

A10: for n being Element of NAT st P_{1}[F_{1}() . n] holds

ex m being Element of NAT st F . m = n_{1}() * F; :: thesis: ( q is subsequence of F_{1}() & ( for n being Nat holds P_{1}[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F_{1}() . n holds

P_{1}[r] ) holds

ex m being Element of NAT st F_{1}() . n = q . m ) )

defpred S_{4}[ set ] means P_{1}[q . $1];

A22: for k being Nat st S_{4}[k] holds

S_{4}[k + 1]
_{1}()
; :: thesis: ( ( for n being Nat holds P_{1}[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F_{1}() . n holds

P_{1}[r] ) holds

ex m being Element of NAT st F_{1}() . n = q . m ) )

A23: S_{4}[ 0 ]
by A3, A9, FUNCT_2:15;

thus for n being Nat holds S_{4}[n]
from NAT_1:sch 2(A23, A22); :: thesis: for n being Element of NAT st ( for r being Real st r = F_{1}() . n holds

P_{1}[r] ) holds

ex m being Element of NAT st F_{1}() . n = q . m

let n be Element of NAT ; :: thesis: ( ( for r being Real st r = F_{1}() . n holds

P_{1}[r] ) implies ex m being Element of NAT st F_{1}() . n = q . m )

assume for r being Real st r = F_{1}() . n holds

P_{1}[r]
; :: thesis: ex m being Element of NAT st F_{1}() . n = q . m

then consider m being Element of NAT such that

A24: F . m = n by A10;

take m ; :: thesis: F_{1}() . n = q . m

thus F_{1}() . n = q . m
by A24, FUNCT_2:15; :: thesis: verum

( n < m & P

m <= k ) );

defpred S

defpred S

ex m1 being Element of NAT st

( 0 <= m1 & P

then A2: ex m being Nat st S

consider M being Nat such that

A3: ( S

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 & P_{1}[F_{1}() . m] )

A6:
for n being Nat( n < m & P

let n be Element of NAT ; :: thesis: ex m being Element of NAT st

( n < m & P_{1}[F_{1}() . m] )

consider m being Element of NAT such that

A5: ( n + 1 <= m & P_{1}[F_{1}() . m] )
by A1;

take m = m; :: thesis: ( n < m & P_{1}[F_{1}() . m] )

thus ( n < m & P_{1}[F_{1}() . m] )
by A5, NAT_1:13; :: thesis: verum

end;( n < m & P

consider m being Element of NAT such that

A5: ( n + 1 <= m & P

take m = m; :: thesis: ( n < m & P

thus ( n < m & P

for x being Element of NAT ex y being Element of NAT st S

proof

consider F being sequence of NAT such that
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S_{2}[n,x,y]

let x be Element of NAT ; :: thesis: ex y being Element of NAT st S_{2}[n,x,y]

defpred S_{4}[ Nat] means ( x < $1 & P_{1}[F_{1}() . $1] );

ex m being Element of NAT st S_{4}[m]
by A4;

then A7: ex m being Nat st S_{4}[m]
;

consider l being Nat such that

A8: ( S_{4}[l] & ( for k being Nat st S_{4}[k] holds

l <= k ) ) from NAT_1:sch 5(A7);

reconsider l = l as Element of NAT by ORDINAL1:def 12;

take l ; :: thesis: S_{2}[n,x,l]

thus S_{2}[n,x,l]
by A8; :: thesis: verum

end;let x be Element of NAT ; :: thesis: ex y being Element of NAT st S

defpred S

ex m being Element of NAT st S

then A7: ex m being Nat st S

consider l being Nat such that

A8: ( S

l <= k ) ) from NAT_1:sch 5(A7);

reconsider l = l as Element of NAT by ORDINAL1:def 12;

take l ; :: thesis: S

thus S

A9: ( F . 0 = M9 & ( for n being Nat holds S

( dom F = NAT & rng F c= REAL ) by FUNCT_2:def 1, NUMBERS:19;

then reconsider F = F as natural-valued Real_Sequence by FUNCT_2:def 1, RELSET_1:4;

for n being Nat holds F . n < F . (n + 1) by A9;

then reconsider F = F as increasing sequence of NAT by SEQM_3:def 6;

A10: for n being Element of NAT st P

ex m being Element of NAT st F . m = n

proof

take q = F
defpred S_{4}[ set ] means ( P_{1}[F_{1}() . $1] & ( for m being Element of NAT holds F . m <> $1 ) );

assume ex n being Element of NAT st S_{4}[n]
; :: thesis: contradiction

then A11: ex n being Nat st S_{4}[n]
;

consider M1 being Nat such that

A12: ( S_{4}[M1] & ( for n being Nat st S_{4}[n] holds

M1 <= n ) ) from NAT_1:sch 5(A11);

defpred S_{5}[ Nat] means ( $1 < M1 & P_{1}[F_{1}() . $1] & ex m being Element of NAT st F . m = $1 );

A13: ex n being Nat st S_{5}[n]
_{5}[n] holds

n <= M1 ;

consider X being Nat such that

A15: ( S_{5}[X] & ( for n being Nat st S_{5}[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 P_{1}[F_{1}() . k]

A19: F . m = X by A15;

A20: ( X < F . (m + 1) & P_{1}[F_{1}() . (F . (m + 1))] )
by A9, A19;

M1 in NAT by ORDINAL1:def 12;

then A21: F . (m + 1) <= M1 by A9, A12, A15, A19;

end;assume ex n being Element of NAT st S

then A11: ex n being Nat st S

consider M1 being Nat such that

A12: ( S

M1 <= n ) ) from NAT_1:sch 5(A11);

defpred S

A13: ex n being Nat st S

proof

A14:
for n being Nat st S
take
M
; :: thesis: S_{5}[M]

( M <= M1 & M <> M1 ) by A3, A9, A12;

hence M < M1 by XXREAL_0:1; :: thesis: ( P_{1}[F_{1}() . M] & ex m being Element of NAT st F . m = M )

thus P_{1}[F_{1}() . 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;( M <= M1 & M <> M1 ) by A3, A9, A12;

hence M < M1 by XXREAL_0:1; :: thesis: ( P

thus P

take 0 ; :: thesis: F . 0 = M

thus F . 0 = M by A9; :: thesis: verum

n <= M1 ;

consider X being Nat such that

A15: ( S

n <= X ) ) from NAT_1:sch 6(A14, A13);

A16: for k being Element of NAT st X < k & k < M1 holds

not P

proof

consider m being Element of NAT such that
given k being Element of NAT such that A17:
X < k
and

A18: ( k < M1 & P_{1}[F_{1}() . k] )
; :: thesis: contradiction

end;A18: ( k < M1 & P

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k )
;

end;

A19: F . m = X by A15;

A20: ( X < F . (m + 1) & P

M1 in NAT by ORDINAL1:def 12;

then A21: F . (m + 1) <= M1 by A9, A12, A15, A19;

now :: thesis: not F . (m + 1) <> M1

hence
contradiction
by A12; :: thesis: verumassume
F . (m + 1) <> M1
; :: thesis: contradiction

then F . (m + 1) < M1 by A21, XXREAL_0:1;

hence contradiction by A16, A20; :: thesis: verum

end;then F . (m + 1) < M1 by A21, XXREAL_0:1;

hence contradiction by A16, A20; :: thesis: verum

P

ex m being Element of NAT st F

defpred S

A22: for k being Nat st S

S

proof

thus
q is subsequence of F
let k be Nat; :: thesis: ( S_{4}[k] implies S_{4}[k + 1] )

assume P_{1}[q . k]
; :: thesis: S_{4}[k + 1]

S_{1}[F . k,F . (k + 1)]
by A9;

then P_{1}[F_{1}() . (F . (k + 1))]
;

hence S_{4}[k + 1]
by FUNCT_2:15; :: thesis: verum

end;assume P

S

then P

hence S

P

ex m being Element of NAT st F

A23: S

thus for n being Nat holds S

P

ex m being Element of NAT st F

let n be Element of NAT ; :: thesis: ( ( for r being Real st r = F

P

assume for r being Real st r = F

P

then consider m being Element of NAT such that

A24: F . m = n by A10;

take m ; :: thesis: F

thus F