let a be Real; 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
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();
take
s
; ( s is convergent & lim s = a & ( for n being Nat holds s . n >= a ) )
set s1 = seq_const a;
set s3 = (seq_const a) + s2;
A4:
s2 is convergent
by A3, SEQ_4:31;
then A5:
(seq_const a) + s2 is convergent
;
lim s2 = 0
by A3, SEQ_4:31;
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; ( lim s = a & ( for n being Nat holds s . n >= a ) )
thus
lim s = a
by A5, A8, A9, A6, SEQ_2:20; for n being Nat holds s . n >= a
let n be Nat; s . n >= a
s . n >= (seq_const a) . n
by A6;
hence
s . n >= a
by SEQ_1:57; verum