let x0 be Real; for seq being Real_Sequence
for f being PartFunc of REAL,REAL st ( for n being Nat holds
( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )
let seq be Real_Sequence; for f being PartFunc of REAL,REAL st ( for n being Nat holds
( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )
let f be PartFunc of REAL,REAL; ( ( for n being Nat holds
( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f ) ) implies ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) ) )
deffunc H1( Nat) -> set = 1 / ($1 + 1);
consider s1 being Real_Sequence such that
A1:
for n being Nat holds s1 . n = H1(n)
from SEQ_1:sch 1();
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set s2 = seq_const x0;
A2:
s1 is convergent
by A1, SEQ_4:31;
then A3:
(seq_const x0) + s1 is convergent
;
assume A4:
for n being Nat holds
( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f )
; ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )
(seq_const x0) . 0 = x0
by SEQ_1:57;
then A7:
lim (seq_const x0) = x0
by SEQ_4:25;
lim s1 = 0
by A1, SEQ_4:31;
then A8: lim ((seq_const x0) + s1) =
x0 + 0
by A7, A2, SEQ_2:6
.=
x0
;
hence
seq is convergent
by A7, A3, A5, SEQ_2:19; ( lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )
thus
lim seq = x0
by A7, A3, A8, A5, SEQ_2:20; ( rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )
hence A9:
rng seq c= dom f
by TARSKI:def 3; rng seq c= (dom f) /\ (right_open_halfline x0)
then
rng seq c= right_open_halfline x0
by TARSKI:def 3;
hence
rng seq c= (dom f) /\ (right_open_halfline x0)
by A9, XBOOLE_1:19; verum