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 H1( Nat) -> set = [\((\$1 + 1) * a)/] / (\$1 + 1);
consider s being Real_Sequence such that
A1: for n being Nat holds s . n = H1(n) from SEQ_1:sch 1();
rng s c= RAT
proof
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:
then consider n being Element of NAT such that
A2: s . n = y by FUNCT_2:113;
s . n = H1(n) by A1;
hence y in RAT by ; :: thesis: verum
end;
then reconsider s = s as Rational_Sequence by RELAT_1:def 19;
deffunc H2( Nat) -> set = 1 / (\$1 + 1);
consider s2 being Real_Sequence such that
A3: for n being Nat holds s2 . n = H2(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 = () - s2;
A4: s2 is convergent by ;
then A5: (seq_const a) - s2 is convergent ;
A6: now :: thesis: for n being Nat holds
( (() - s2) . n <= s . n & s . n <= () . n )
let n be Nat; :: thesis: ( (() - s2) . n <= s . n & s . n <= () . 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) <= () . n by SEQ_1:57;
hence ( ((seq_const a) - s2) . n <= s . n & s . n <= () . n ) by ; :: thesis: verum
end;
lim s2 = 0 by ;
then A8: lim (() - s2) = (() . 0) - 0 by
.= a by SEQ_1:57 ;
A9: lim () = () . 0 by SEQ_4:26
.= a by SEQ_1:57 ;
hence s is convergent by ; :: 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 <= () . n by A6;
hence s . n <= a by SEQ_1:57; :: thesis: verum