let a be Real; :: thesis: ex s being Rational_Sequence st

( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )

deffunc H_{1}( Nat) -> set = [\(($1 + 1) * a)/] / ($1 + 1);

consider s being Real_Sequence such that

A1: for n being Nat holds s . n = H_{1}(n)
from SEQ_1:sch 1();

rng s c= RAT

deffunc H_{2}( Nat) -> set = 1 / ($1 + 1);

consider s2 being Real_Sequence such that

A3: for n being Nat holds s2 . n = H_{2}(n)
from SEQ_1:sch 1();

reconsider a1 = a as Element of REAL by XREAL_0:def 1;

set s1 = seq_const a;

take s ; :: thesis: ( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )

set s3 = (seq_const a) - s2;

A4: s2 is convergent by A3, SEQ_4:31;

then A5: (seq_const a) - s2 is convergent ;

then A8: lim ((seq_const a) - s2) = ((seq_const a) . 0) - 0 by A4, SEQ_4:42

.= a by SEQ_1:57 ;

A9: lim (seq_const a) = (seq_const a) . 0 by SEQ_4:26

.= a by SEQ_1:57 ;

hence s is convergent by A5, A8, A6, SEQ_2:19; :: thesis: ( lim s = a & ( for n being Nat holds s . n <= a ) )

thus lim s = a by A5, A8, A9, A6, SEQ_2:20; :: thesis: for n being Nat holds s . n <= a

let n be Nat; :: thesis: s . n <= a

s . n <= (seq_const a) . n by A6;

hence s . n <= a by SEQ_1:57; :: thesis: verum

( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )

deffunc H

consider s being Real_Sequence such that

A1: for n being Nat holds s . n = H

rng s c= RAT

proof

then reconsider s = s as Rational_Sequence by RELAT_1:def 19;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in RAT )

assume y in rng s ; :: thesis: y in RAT

then consider n being Element of NAT such that

A2: s . n = y by FUNCT_2:113;

s . n = H_{1}(n)
by A1;

hence y in RAT by A2, RAT_1:def 2; :: thesis: verum

end;assume y in rng s ; :: thesis: y in RAT

then consider n being Element of NAT such that

A2: s . n = y by FUNCT_2:113;

s . n = H

hence y in RAT by A2, RAT_1:def 2; :: thesis: verum

deffunc H

consider s2 being Real_Sequence such that

A3: for n being Nat holds s2 . n = H

reconsider a1 = a as Element of REAL by XREAL_0:def 1;

set s1 = seq_const a;

take s ; :: thesis: ( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )

set s3 = (seq_const a) - s2;

A4: s2 is convergent by A3, SEQ_4:31;

then A5: (seq_const a) - s2 is convergent ;

A6: now :: thesis: for n being Nat holds

( ((seq_const a) - s2) . n <= s . n & s . n <= (seq_const a) . n )

lim s2 = 0
by A3, SEQ_4:31;( ((seq_const a) - s2) . n <= s . n & s . n <= (seq_const a) . n )

let n be Nat; :: thesis: ( ((seq_const a) - s2) . n <= s . n & s . n <= (seq_const a) . n )

(n + 1) * a <= [\((n + 1) * a)/] + 1 by INT_1:29;

then ((n + 1) * a) - 1 <= ([\((n + 1) * a)/] + 1) - 1 by XREAL_1:9;

then (((n + 1) * a) - 1) * ((n + 1) ") <= [\((n + 1) * a)/] / (n + 1) by XREAL_1:64;

then ((a / (n + 1)) * (n + 1)) - (1 / (n + 1)) <= s . n by A1;

then a - (1 / (n + 1)) <= s . n by XCMPLX_1:87;

then ((seq_const a) . n) - (1 / (n + 1)) <= s . n by SEQ_1:57;

then A7: ((seq_const a) . n) - (s2 . n) <= s . n by A3;

[\((n + 1) * a)/] <= (n + 1) * a by INT_1:def 6;

then [\((n + 1) * a)/] * ((n + 1) ") <= (a * (n + 1)) * ((n + 1) ") by XREAL_1:64;

then [\((n + 1) * a)/] * ((n + 1) ") <= a * ((n + 1) * ((n + 1) ")) ;

then [\((n + 1) * a)/] * ((n + 1) ") <= a * 1 by XCMPLX_0:def 7;

then [\((n + 1) * a)/] / (n + 1) <= (seq_const a) . n by SEQ_1:57;

hence ( ((seq_const a) - s2) . n <= s . n & s . n <= (seq_const a) . n ) by A1, A7, RFUNCT_2:1; :: thesis: verum

end;(n + 1) * a <= [\((n + 1) * a)/] + 1 by INT_1:29;

then ((n + 1) * a) - 1 <= ([\((n + 1) * a)/] + 1) - 1 by XREAL_1:9;

then (((n + 1) * a) - 1) * ((n + 1) ") <= [\((n + 1) * a)/] / (n + 1) by XREAL_1:64;

then ((a / (n + 1)) * (n + 1)) - (1 / (n + 1)) <= s . n by A1;

then a - (1 / (n + 1)) <= s . n by XCMPLX_1:87;

then ((seq_const a) . n) - (1 / (n + 1)) <= s . n by SEQ_1:57;

then A7: ((seq_const a) . n) - (s2 . n) <= s . n by A3;

[\((n + 1) * a)/] <= (n + 1) * a by INT_1:def 6;

then [\((n + 1) * a)/] * ((n + 1) ") <= (a * (n + 1)) * ((n + 1) ") by XREAL_1:64;

then [\((n + 1) * a)/] * ((n + 1) ") <= a * ((n + 1) * ((n + 1) ")) ;

then [\((n + 1) * a)/] * ((n + 1) ") <= a * 1 by XCMPLX_0:def 7;

then [\((n + 1) * a)/] / (n + 1) <= (seq_const a) . n by SEQ_1:57;

hence ( ((seq_const a) - s2) . n <= s . n & s . n <= (seq_const a) . n ) by A1, A7, RFUNCT_2:1; :: thesis: verum

then A8: lim ((seq_const a) - s2) = ((seq_const a) . 0) - 0 by A4, SEQ_4:42

.= a by SEQ_1:57 ;

A9: lim (seq_const a) = (seq_const a) . 0 by SEQ_4:26

.= a by SEQ_1:57 ;

hence s is convergent by A5, A8, A6, SEQ_2:19; :: thesis: ( lim s = a & ( for n being Nat holds s . n <= a ) )

thus lim s = a by A5, A8, A9, A6, SEQ_2:20; :: thesis: for n being Nat holds s . n <= a

let n be Nat; :: thesis: s . n <= a

s . n <= (seq_const a) . n by A6;

hence s . n <= a by SEQ_1:57; :: thesis: verum