let f be PartFunc of REAL ,REAL ; :: thesis: for x0 being Real st ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) holds
ex h being convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) )
let x0 be Real; :: thesis: ( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) implies ex h being convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) ) )
given r being Real such that A1: r > 0 and
A2: [.x0,(x0 + r).] c= dom f ; :: thesis: ex h being convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) )
reconsider a = NAT --> x0 as Real_Sequence ;
reconsider a = a as V8() Real_Sequence ;
deffunc H₁( Element of NAT ) -> Element of REAL = r / ($1 + 2);
consider b being Real_Sequence such that
A3: for n being Element of NAT holds b . n = H₁(n) from SEQ_1:sch 1();

A4: now

let n be Element of NAT ; :: thesis: 0 < b . n
0 <= n by NAT_1:2;
then 0 < r / (n + 2) by A1, XREAL_1:141;
hence 0 < b . n by A3; :: thesis: verum

end;

then for n being Element of NAT holds 0 <> b . n ;
then A5: b is non-zero by SEQ_1:7;
( b is convergent & lim b = 0 ) by A3, SEQ_4:46;
then reconsider b = b as convergent_to_0 Real_Sequence by A5, FDIFF_1:def 1;
take b ; :: thesis: ex c being V8() Real_Sequence st
( rng c = {x0} & rng (b + c) c= dom f & ( for n being Element of NAT holds b . n > 0 ) )
take a ; :: thesis: ( rng a = {x0} & rng (b + a) c= dom f & ( for n being Element of NAT holds b . n > 0 ) )
thus rng a = {x0} :: thesis: ( rng (b + a) c= dom f & ( for n being Element of NAT holds b . n > 0 ) )

proof

thus rng a c= {x0} :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in {x0} )
assume x in rng a ; :: thesis: x in {x0}
then ex n being Element of NAT st x = a . n by FUNCT_2:190;
then x = x0 by FUNCOP_1:13;
hence x in {x0} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in rng a )
assume x in {x0} ; :: thesis: x in rng a
then x = x0 by TARSKI:def 1
.= a . 0 by FUNCOP_1:13 ;
hence x in rng a by VALUED_0:28; :: thesis: verum

end;

thus rng (b + a) c= dom f :: thesis: for n being Element of NAT holds b . n > 0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (b + a) or x in dom f )
assume x in rng (b + a) ; :: thesis: x in dom f
then consider n being Element of NAT such that
A6: x = (b + a) . n by FUNCT_2:190;
A7: 0 + 1 < n + 2 by NAT_1:2, XREAL_1:10;
then r * 1 < r * (n + 2) by A1, XREAL_1:99;
then r * ((n + 2) " ) < (r * (n + 2)) * ((n + 2) " ) by A7, XREAL_1:70;
then r * ((n + 2) " ) < r * ((n + 2) * ((n + 2) " )) ;
then r * ((n + 2) " ) < r * 1 by A7, XCMPLX_0:def 7;
then r / (n + 2) < r by XCMPLX_0:def 9;
then A8: x0 + (r / (n + 2)) <= x0 + r by XREAL_1:8;
0 < r / (n + 2) by A1, A7, XREAL_1:141;
then x0 + 0 < x0 + (r / (n + 2)) by XREAL_1:10;
then A9: x0 + (r / (n + 2)) in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r ) } by A8;
x = (b . n) + (a . n) by A6, SEQ_1:11
.= (r / (n + 2)) + (a . n) by A3
.= (r / (n + 2)) + x0 by FUNCOP_1:13 ;
then x in [.x0,(x0 + r).] by A9, RCOMP_1:def 1;
hence x in dom f by A2; :: thesis: verum

end;

thus for n being Element of NAT holds b . n > 0 by A4; :: thesis: verum