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

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

let n be Nat; :: thesis: b . n < 0
0 < r / (n + 2) by A1, XREAL_1:139;
then - (r / (n + 2)) < - 0 by XREAL_1:24;
then (- r) / (n + 2) < 0 by XCMPLX_1:187;
hence b . n < 0 by A3; :: thesis: verum

end;

then for n being Nat holds 0 <> b . n ;
then A5: b is non-zero by SEQ_1:5;
( b is convergent & lim b = 0 ) by A3, SEQ_4:31;
then reconsider b = b as non-zero 0 -convergent Real_Sequence by A5, FDIFF_1:def 1;
take b ; :: thesis: ex c being constant Real_Sequence st
( rng c = {x0} & rng (b + c) c= dom f & ( for n being Nat holds b . n < 0 ) )
take a ; :: thesis: ( rng a = {x0} & rng (b + a) c= dom f & ( for n being Nat holds b . n < 0 ) )
thus rng a = {x0} :: thesis: ( rng (b + a) c= dom f & ( for n being 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 object ; :: 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:113;
then x = x0 by SEQ_1:57;
hence x in {x0} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 SEQ_1:57 ;
hence x in rng a by VALUED_0:28; :: thesis: verum

end;

thus rng (b + a) c= dom f :: thesis: for n being Nat holds b . n < 0

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
A6: x = (b + a) . n by FUNCT_2:113;
0 + 1 < n + 2 by XREAL_1:8;
then r * 1 < r * (n + 2) by A1, XREAL_1:97;
then r * ((n + 2) ") < (r * (n + 2)) * ((n + 2) ") by XREAL_1:68;
then r * ((n + 2) ") < r * ((n + 2) * ((n + 2) ")) ;
then r * ((n + 2) ") < r * 1 by XCMPLX_0:def 7;
then r / (n + 2) < r by XCMPLX_0:def 9;
then x0 - r < x0 - (r / (n + 2)) by XREAL_1:15;
then x0 - r < x0 + (- (r / (n + 2))) ;
then A7: x0 - r <= x0 + ((- r) / (n + 2)) by XCMPLX_1:187;
0 < r / (n + 2) by A1, XREAL_1:139;
then x0 - (r / (n + 2)) < x0 - 0 by XREAL_1:15;
then x0 + (- (r / (n + 2))) <= x0 ;
then x0 + ((- r) / (n + 2)) <= x0 by XCMPLX_1:187;
then A8: x0 + ((- r) / (n + 2)) in { g1 where g1 is Real : ( x0 - r <= g1 & g1 <= x0 ) } by A7;
x = (b . n) + (a . n) by A6, SEQ_1:7
.= ((- r) / (n + 2)) + (a . n) by A3
.= x0 + ((- r) / (n + 2)) by SEQ_1:57 ;
then x in [.(x0 - r),x0.] by A8, RCOMP_1:def 1;
hence x in dom f by A2; :: thesis: verum

end;

thus for n being Nat holds b . n < 0 by A4; :: thesis: verum