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
s . n = [\((n + 1) * a)/] / (n + 1) by A1;
hence s . n is Rational ; :: thesis: verum

end;

then reconsider s = s as Rational_Sequence by Def6;
take s ; :: thesis: ( s is convergent & lim s = a & ( for n being Element of NAT holds s . n <= a ) )
reconsider a1 = a as Real by XREAL_0:def 1;
reconsider s1 = NAT --> a1 as Real_Sequence ;
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();
A3: ( s2 is convergent & lim s2 = 0 ) by A2, SEQ_4:45;
set s3 = s1 - s2;
A5: s1 - s2 is convergent by A3, SEQ_2:25;
A6: lim (s1 - s2) = (s1 . 0 ) - 0 by A3, SEQ_4:59
.= a by FUNCOP_1:13 ;
A7: lim s1 = s1 . 0 by SEQ_4:41
.= a by FUNCOP_1:13 ;

A8: now

let n be Element of NAT ; :: thesis: ( (s1 - s2) . n <= s . n & s . n <= s1 . n )
[\((n + 1) * a)/] <= (n + 1) * a by INT_1:def 4;
then [\((n + 1) * a)/] * ((n + 1) " ) <= (a * (n + 1)) * ((n + 1) " ) by XREAL_1:66;
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) <= a ;
then A9: [\((n + 1) * a)/] / (n + 1) <= s1 . n by FUNCOP_1:13;
(n + 1) * a <= [\((n + 1) * a)/] + 1 by INT_1:52;
then ((n + 1) * a) - 1 <= ([\((n + 1) * a)/] + 1) - 1 by XREAL_1:11;
then (((n + 1) * a) - 1) * ((n + 1) " ) <= [\((n + 1) * a)/] * ((n + 1) " ) by XREAL_1:66;
then (((n + 1) * a) - 1) * ((n + 1) " ) <= [\((n + 1) * a)/] / (n + 1) ;
then (((n + 1) * a) - 1) * ((n + 1) " ) <= s . n by A1;
then (((n + 1) * a) - 1) / (n + 1) <= s . n ;
then (((n + 1) * a) / (n + 1)) - (1 / (n + 1)) <= s . n ;
then ((a / (n + 1)) * (n + 1)) - (1 / (n + 1)) <= s . n ;
then a - (1 / (n + 1)) <= s . n by XCMPLX_1:88;
then (s1 . n) - (1 / (n + 1)) <= s . n by FUNCOP_1:13;
then (s1 . n) - (s2 . n) <= s . n by A2;
hence ( (s1 - s2) . n <= s . n & s . n <= s1 . n ) by A1, A9, RFUNCT_2:6; :: thesis: verum

end;

hence s is convergent by A5, A6, A7, SEQ_2:33; :: thesis: ( lim s = a & ( for n being Element of NAT holds s . n <= a ) )
thus lim s = a by A5, A6, A7, A8, SEQ_2:34; :: 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 A8;
hence s . n <= a by FUNCOP_1:13; :: thesis: verum