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 non-zero 0 -convergent Real_Sequence ex c being constant 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 non-zero 0 -convergent Real_Sequence ex c being constant 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 non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st
( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f )
reconsider r0 = r as Element of REAL by XREAL_0:def 1;
set a = seq_const r;
consider g being Real such that
A2: 0 < g and
A3: N = ].(r - g),(r + g).[ by RCOMP_1:def 6;
reconsider a = seq_const r as constant Real_Sequence ;
deffunc H₁( Nat) -> set = g / ($1 + 2);
consider b being Real_Sequence such that
A4: for n being Nat holds b . n = H₁(n) from SEQ_1:sch 1();
A5: lim b = 0 by A4, SEQ_4:31;
A6: b is convergent by A4, SEQ_4:31;

now :: thesis: for n being Nat holds 0 <> b . n

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

end;

then b is non-zero by SEQ_1:5;
then reconsider b = b as non-zero 0 -convergent Real_Sequence by A6, A5, FDIFF_1:def 1;
take b ; :: thesis: ex c being constant 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 object ; :: 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:113;
then x = r by SEQ_1:57;
hence x in {r} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 SEQ_1:57 ;
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 object ; :: 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:113;
0 + 1 < n + 2 by XREAL_1:8;
then g * 1 < g * (n + 2) by A2, XREAL_1:97;
then g * ((n + 2) ") < (g * (n + 2)) * ((n + 2) ") by XREAL_1:68;
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:6;
A9: r - g < r - 0 by A2, XREAL_1:15;
r + 0 < r + (g / (n + 2)) by A2, XREAL_1:8;
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:7
.= (g / (n + 2)) + (a . n) by A4
.= (g / (n + 2)) + r by SEQ_1:57 ;
then x in N by A3, A10, RCOMP_1:def 2;
hence x in dom f by A1; :: thesis: verum

end;

let x be object ; :: 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:16;
hence x in dom f by A1; :: thesis: verum