let x, r be Real; :: thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st r > 0 & rng c = {x} & ( for n being Nat holds h . n < 0 ) holds
ex N being Nat st
( rng ((h ^\ N) + c) c= ].(x - r),x.[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) )
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st r > 0 & rng c = {x} & ( for n being Nat holds h . n < 0 ) holds
ex N being Nat st
( rng ((h ^\ N) + c) c= ].(x - r),x.[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) )
let c be constant Real_Sequence; :: thesis: ( r > 0 & rng c = {x} & ( for n being Nat holds h . n < 0 ) implies ex N being Nat st
( rng ((h ^\ N) + c) c= ].(x - r),x.[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) ) )
assume that
A1: r > 0 and
A2: rng c = {x} and
A3: for n being Nat holds h . n < 0 ; :: thesis: ex N being Nat st
( rng ((h ^\ N) + c) c= ].(x - r),x.[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) )
( h is convergent & lim h = 0 ) ;
then consider N being Nat such that
A4: for m being Nat st N <= m holds
|.((h . m) - 0).| < r by A1, SEQ_2:def 7;
take N ; :: thesis: ( rng ((h ^\ N) + c) c= ].(x - r),x.[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) )
set h1 = h ^\ N;

now :: thesis: for p being Real st p in rng ((h ^\ N) + c) holds
p in ].(x - r),x.[

let p be Real; :: thesis: ( p in rng ((h ^\ N) + c) implies p in ].(x - r),x.[ )
assume p in rng ((h ^\ N) + c) ; :: thesis: p in ].(x - r),x.[
then consider k being Element of NAT such that
A5: p = ((h ^\ N) + c) . k by FUNCT_2:113;
A6: p = ((h ^\ N) . k) + (c . k) by A5, VALUED_1:1;
c . k in rng c by FUNCT_2:112;
then A7: c . k = x by A2, TARSKI:def 1;
A8: (h ^\ N) . k = h . (N + k) by NAT_1:def 3;
|.(((h ^\ N) . k) - 0).| < r by A4, A8, NAT_1:11;
then - ((h ^\ N) . k) < r by A3, A8, ABSVALUE:def 1;
then ( x - r < p & p < x ) by A3, A8, A6, A7, XREAL_1:6, XREAL_1:25, XREAL_1:30;
hence p in ].(x - r),x.[ by XXREAL_1:4; :: thesis: verum

end;

hence A9: rng ((h ^\ N) + c) c= ].(x - r),x.[ ; :: thesis: ( ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) )
thus A10: for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) :: thesis: for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x )

proof

let m be Nat; :: thesis: ((h ^\ N) + c) . m = (h + c) . (N + m)
A11: ( dom ((h ^\ N) + c) = NAT & dom c = NAT & dom (h + c) = NAT ) by FUNCT_2:def 1;
then ( m in dom ((h ^\ N) + c) & m in dom c & N + m in dom (h + c) & N + m in dom c ) by ORDINAL1:def 12;
then A12: c . m = c . (N + m) by FUNCT_1:def 10;
((h ^\ N) + c) . m = ((h ^\ N) . m) + (c . m) by A11, ORDINAL1:def 12, VALUED_1:def 1
.= (h . (N + m)) + (c . (N + m)) by A12, NAT_1:def 3 ;
hence ((h ^\ N) + c) . m = (h + c) . (N + m) by A11, ORDINAL1:def 12, VALUED_1:def 1; :: thesis: verum

end;

thus for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) :: thesis: verum

proof

let m be Nat; :: thesis: ( N <= m implies ( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) )
assume A13: N <= m ; :: thesis: ( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x )
then |.((h . m) - 0).| < r by A4;
hence |.(h . m).| < r ; :: thesis: ( x - r < (h + c) . m & (h + c) . m < x )
consider m1 being Nat such that
A14: m = N + m1 by A13, NAT_1:10;
dom ((h ^\ N) + c) = NAT by FUNCT_2:def 1;
then ((h ^\ N) + c) . m1 in rng ((h ^\ N) + c) by FUNCT_1:3, ORDINAL1:def 12;
then ( x - r < ((h ^\ N) + c) . m1 & ((h ^\ N) + c) . m1 < x ) by A9, XXREAL_1:4;
hence ( x - r < (h + c) . m & (h + c) . m < x ) by A14, A10; :: thesis: verum

end;