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 H1( Nat) -> set = r / ($1 + 2);
consider b being Real_Sequence such that
A3: for n being Nat holds b . n = H1(n) from SEQ_1:sch 1();
A4: now :: thesis: 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;
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 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;
thus for n being Nat holds b . n > 0 by A4; :: thesis: verum