let a be real number ; :: thesis: ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Element of NAT holds s . n >= a ) )
deffunc H₁( Element of NAT ) -> Element of REAL = [/(($1 + 1) * a)\] / ($1 + 1);
consider s being Real_Sequence such that
A1: for n being Element of NAT holds s . n = H₁(n) from SEQ_1:sch 1();

now

let n be Element of NAT ; :: thesis: s . n is Rational
[/((n + 1) * a)\] / (n + 1) = s . n by A1;
hence s . n is Rational ; :: thesis: verum

end;

then reconsider s = s as Rational_Sequence by Def6;
deffunc H₂( Element of NAT ) -> Element of REAL = 1 / ($1 + 1);
consider s2 being Real_Sequence such that
A2: for n being Element of NAT holds s2 . n = H₂(n) from SEQ_1:sch 1();
take s ; :: thesis: ( s is convergent & lim s = a & ( for n being Element of NAT holds s . n >= a ) )
a in REAL by XREAL_0:def 1;
then reconsider s1 = NAT --> a as Real_Sequence by FUNCOP_1:45;
set s3 = s1 + s2;
A3: s2 is convergent by A2, SEQ_4:30;
then A4: s1 + s2 is convergent by SEQ_2:5;

A5: now

let n be Element of NAT ; :: thesis: ( s1 . n <= s . n & s . n <= (s1 + s2) . n )
((n + 1) * a) + 1 >= [/((n + 1) * a)\] by INT_1:def 7;
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 (s1 . n) + (1 / (n + 1)) >= s . n by FUNCOP_1:7;
then A6: (s1 . n) + (s2 . n) >= s . n by A2;
[/((n + 1) * a)\] >= (n + 1) * a by INT_1:def 7;
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) >= s1 . n by FUNCOP_1:7;
hence ( s1 . n <= s . n & s . n <= (s1 + s2) . n ) by A1, A6, SEQ_1:7; :: thesis: verum

end;

lim s2 = 0 by A2, SEQ_4:30;
then A7: lim (s1 + s2) = (s1 . 0) + 0 by A3, SEQ_4:42
.= a by FUNCOP_1:7 ;
A8: lim s1 = s1 . 0 by SEQ_4:26
.= a by FUNCOP_1:7 ;
hence s is convergent by A4, A7, A5, SEQ_2:19; :: thesis: ( lim s = a & ( for n being Element of NAT holds s . n >= a ) )
thus lim s = a by A4, A7, A8, A5, SEQ_2:20; :: thesis: for n being Element of NAT holds s . n >= a
let n be Element of NAT ; :: thesis: s . n >= a
s . n >= s1 . n by A5;
hence s . n >= a by FUNCOP_1:7; :: thesis: verum