let r be Real; :: thesis: for f being PartFunc of REAL ,REAL st ex N being Neighbourhood of r st N c= dom f holds
ex h being convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f )
let f be PartFunc of REAL ,REAL ; :: thesis: ( ex N being Neighbourhood of r st N c= dom f implies ex h being convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f ) )
given N being Neighbourhood of r such that A1: N c= dom f ; :: thesis: ex h being convergent_to_0 Real_Sequence ex c being V8() Real_Sequence st
( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f )
reconsider a = NAT --> r as Real_Sequence by FUNCOP_1:57;
consider g being real number such that
A2: 0 < g and
A3: N = ].(r - g),(r + g).[ by RCOMP_1:def 7;
reconsider a = a as V8() Real_Sequence ;
deffunc H₁( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider b being Real_Sequence such that
A4: for n being Element of NAT holds b . n = H₁(n) from SEQ_1:sch 1();
A5: lim b = 0 by A4, SEQ_4:46;
A6: b is convergent by A4, SEQ_4:46;

now

let n be Element of NAT ; :: thesis: 0 <> b . n
0 < g / (n + 2) by A2;
hence 0 <> b . n by A4; :: thesis: verum

end;

then b is non-empty by SEQ_1:7;
then reconsider b = b as convergent_to_0 Real_Sequence by A6, A5, FDIFF_1:def 1;
take b ; :: thesis: ex c being V8() Real_Sequence st
( rng c = {r} & rng (b + c) c= dom f & {r} c= dom f )
take a ; :: thesis: ( rng a = {r} & rng (b + a) c= dom f & {r} c= dom f )
thus rng a = {r} :: thesis: ( rng (b + a) c= dom f & {r} c= dom f )

proof

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

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {r} or x in rng a )
assume x in {r} ; :: thesis: x in rng a
then x = r 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: {r} c= dom f

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
A7: x = (b + a) . n by FUNCT_2:190;
0 + 1 < n + 2 by XREAL_1:10;
then g * 1 < g * (n + 2) by A2, XREAL_1:99;
then g * ((n + 2) " ) < (g * (n + 2)) * ((n + 2) " ) by XREAL_1:70;
then g * ((n + 2) " ) < g * ((n + 2) * ((n + 2) " )) ;
then g * ((n + 2) " ) < g * 1 by XCMPLX_0:def 7;
then g / (n + 2) < g by XCMPLX_0:def 9;
then A8: r + (g / (n + 2)) < r + g by XREAL_1:8;
A9: r - g < r - 0 by A2, XREAL_1:17;
r + 0 < r + (g / (n + 2)) by A2, XREAL_1:10;
then r - g < r + (g / (n + 2)) by A9, XXREAL_0:2;
then A10: r + (g / (n + 2)) in { g1 where g1 is Real : ( r - g < g1 & g1 < r + g ) } by A8;
x = (b . n) + (a . n) by A7, SEQ_1:11
.= (g / (n + 2)) + (a . n) by A4
.= (g / (n + 2)) + r by FUNCOP_1:13 ;
then x in N by A3, A10, RCOMP_1:def 2;
hence x in dom f by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {r} or x in dom f )
assume x in {r} ; :: thesis: x in dom f
then x = r by TARSKI:def 1;
then x in N by RCOMP_1:37;
hence x in dom f by A1; :: thesis: verum