let x0 be Real; :: thesis: for seq being Real_Sequence
for f being PartFunc of REAL ,REAL st ( for n being Element of NAT holds
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) )
let seq be Real_Sequence; :: thesis: for f being PartFunc of REAL ,REAL st ( for n being Element of NAT holds
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( ( for n being Element of NAT holds
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) implies ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) ) )
deffunc H₁( Element of NAT ) -> Element of REAL = 1 / ($1 + 1);
consider s1 being Real_Sequence such that
A1: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();
reconsider s2 = NAT --> x0 as Real_Sequence ;
A2: s1 is convergent by A1, SEQ_4:45;
then A3: s2 - s1 is convergent by SEQ_2:25;
assume A4: for n being Element of NAT holds
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) )

A5: now

let n be Element of NAT ; :: thesis: ( (s2 - s1) . n <= seq . n & seq . n <= s2 . n )
A6: (s2 - s1) . n = (s2 . n) - (s1 . n) by RFUNCT_2:6
.= x0 - (s1 . n) by FUNCOP_1:13
.= x0 - (1 / (n + 1)) by A1 ;
seq . n <= x0 by A4;
hence ( (s2 - s1) . n <= seq . n & seq . n <= s2 . n ) by A4, A6, FUNCOP_1:13; :: thesis: verum

end;

s2 . 0 = x0 by FUNCOP_1:13;
then A7: lim s2 = x0 by SEQ_4:40;
lim s1 = 0 by A1, SEQ_4:45;
then A8: lim (s2 - s1) = x0 - 0 by A7, A2, SEQ_2:26
.= x0 ;
hence seq is convergent by A7, A3, A5, SEQ_2:33; :: thesis: ( lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) )
thus lim seq = x0 by A7, A3, A8, A5, SEQ_2:34; :: thesis: ( rng seq c= dom f & rng seq c= (dom f) /\ (left_open_halfline x0) )

now

let x be set ; :: 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:190;
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) /\ (left_open_halfline x0)

now

let x be set ; :: thesis: ( x in rng seq implies x in left_open_halfline x0 )
assume x in rng seq ; :: thesis: x in left_open_halfline x0
then consider n being Element of NAT such that
A10: x = seq . n by FUNCT_2:190;
seq . n < x0 by A4;
then seq . n in { g2 where g2 is Real : g2 < x0 } ;
hence x in left_open_halfline x0 by A10, XXREAL_1:229; :: thesis: verum

end;

then rng seq c= left_open_halfline x0 by TARSKI:def 3;
hence rng seq c= (dom f) /\ (left_open_halfline x0) by A9, XBOOLE_1:19; :: thesis: verum