let x0 be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )
A5: now :: thesis: for n being Nat holds
( (seq_const x0) . n <= seq . n & seq . n <= ((seq_const x0) + s1) . n )
let n be Nat; :: thesis: ( (seq_const x0) . n <= seq . n & seq . n <= ((seq_const x0) + s1) . n )
A6: ((seq_const x0) + s1) . n = ((seq_const x0) . n) + (s1 . n) by SEQ_1:7
.= x0 + (s1 . n) by SEQ_1:57
.= x0 + (1 / (n + 1)) by A1 ;
x0 <= seq . n by A4;
hence ( (seq_const x0) . n <= seq . n & seq . n <= ((seq_const x0) + s1) . n ) by A4, A6, SEQ_1:57; :: thesis: verum
end;
(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; :: thesis: ( 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; :: thesis: ( rng seq c= dom f & rng seq c= (dom f) /\ (right_open_halfline x0) )
now :: thesis: for x being object st x in rng seq holds
x in dom f
let x be object ; :: thesis: ( x in rng seq implies x in dom f )
assume x in rng seq ; :: thesis: x in dom f
then ex n being Element of NAT st seq . n = x by FUNCT_2:113;
hence x in dom f by A4; :: thesis: verum
end;
hence A9: rng seq c= dom f by TARSKI:def 3; :: thesis: rng seq c= (dom f) /\ (right_open_halfline x0)
now :: thesis: for x being object st x in rng seq holds
x in right_open_halfline x0
let x be object ; :: thesis: ( x in rng seq implies x in right_open_halfline x0 )
assume x in rng seq ; :: thesis: x in right_open_halfline x0
then consider n being Element of NAT such that
A10: x = seq . n by FUNCT_2:113;
x0 < seq . n by A4;
then seq . n in { g2 where g2 is Real : x0 < g2 } ;
hence x in right_open_halfline x0 by A10, XXREAL_1:230; :: thesis: verum
end;
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; :: thesis: verum