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 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,(x0 + r).] 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,(x0 + r).] 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_{1}( Nat) -> set = r / ($1 + 2);

consider b being Real_Sequence such that

A3: for n being Nat holds b . n = H_{1}(n)
from SEQ_1:sch 1();

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 ) )

( r > 0 & [.x0,(x0 + r).] 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,(x0 + r).] 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,(x0 + r).] 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

consider b being Real_Sequence such that

A3: for n being Nat holds b . n = H

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

then
for n being Nat holds 0 <> b . n
;let n be Nat; :: thesis: 0 < b . n

0 < r / (n + 2) by A1, XREAL_1:139;

hence 0 < b . n by A3; :: thesis: verum

end;0 < r / (n + 2) by A1, XREAL_1:139;

hence 0 < b . n by A3; :: thesis: verum

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 (b + a) c= dom f
:: thesis: for n being Nat holds b . n > 0
thus
rng a c= {x0}
:: according to XBOOLE_0:def 10 :: thesis: {x0} c= 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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in rng a )
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;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

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

proof

thus
for n being Nat holds b . n > 0
by A4; :: thesis: verum
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 A7: x0 + (r / (n + 2)) <= x0 + r by XREAL_1:6;

0 < r / (n + 2) by A1, XREAL_1:139;

then x0 + 0 < x0 + (r / (n + 2)) by XREAL_1:8;

then A8: x0 + (r / (n + 2)) in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r ) } by A7;

x = (b . n) + (a . n) by A6, SEQ_1:7

.= (r / (n + 2)) + (a . n) by A3

.= (r / (n + 2)) + x0 by SEQ_1:57 ;

then x in [.x0,(x0 + r).] by A8, RCOMP_1:def 1;

hence x in dom f by A2; :: thesis: verum

end;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 A7: x0 + (r / (n + 2)) <= x0 + r by XREAL_1:6;

0 < r / (n + 2) by A1, XREAL_1:139;

then x0 + 0 < x0 + (r / (n + 2)) by XREAL_1:8;

then A8: x0 + (r / (n + 2)) in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r ) } by A7;

x = (b . n) + (a . n) by A6, SEQ_1:7

.= (r / (n + 2)) + (a . n) by A3

.= (r / (n + 2)) + x0 by SEQ_1:57 ;

then x in [.x0,(x0 + r).] by A8, RCOMP_1:def 1;

hence x in dom f by A2; :: thesis: verum