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,(x + r).[ & ( 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 < (h + c) . m & (h + c) . m < x + r ) ) )
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,(x + r).[ & ( 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 < (h + c) . m & (h + c) . m < x + r ) ) )
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,(x + r).[ & ( 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 < (h + c) . m & (h + c) . m < x + r ) ) ) )
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,(x + r).[ & ( 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 < (h + c) . m & (h + c) . m < x + r ) ) )
( 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,(x + r).[ & ( 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 < (h + c) . m & (h + c) . m < x + r ) ) )
set h1 = h ^\ N;

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

let p be Real; :: thesis: ( p in rng ((h ^\ N) + c) implies p in ].x,(x + r).[ )
assume p in rng ((h ^\ N) + c) ; :: thesis: p in ].x,(x + r).[
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;
then A9: (h ^\ N) . k > 0 by A3;
|.(((h ^\ N) . k) - 0).| < r by A4, A8, NAT_1:11;
then (h ^\ N) . k < r by A9, ABSVALUE:def 1;
then ( x < p & p < x + r ) by A3, A8, A6, A7, XREAL_1:6, XREAL_1:29;
hence p in ].x,(x + r).[ by XXREAL_1:4; :: thesis: verum

end;

hence A10: rng ((h ^\ N) + c) c= ].x,(x + r).[ ; :: 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 < (h + c) . m & (h + c) . m < x + r ) ) )
thus A11: 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 < (h + c) . m & (h + c) . m < x + r )

proof

let m be Nat; :: thesis: ((h ^\ N) + c) . m = (h + c) . (N + m)
A12: ( 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 A13: c . m = c . (N + m) by FUNCT_1:def 10;
((h ^\ N) + c) . m = ((h ^\ N) . m) + (c . m) by A12, ORDINAL1:def 12, VALUED_1:def 1
.= (h . (N + m)) + (c . (N + m)) by A13, NAT_1:def 3 ;
hence ((h ^\ N) + c) . m = (h + c) . (N + m) by A12, ORDINAL1:def 12, VALUED_1:def 1; :: thesis: verum

end;

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

proof

let m be Nat; :: thesis: ( N <= m implies ( |.(h . m).| < r & x < (h + c) . m & (h + c) . m < x + r ) )
assume A14: N <= m ; :: thesis: ( |.(h . m).| < r & x < (h + c) . m & (h + c) . m < x + r )
then |.((h . m) - 0).| < r by A4;
hence |.(h . m).| < r ; :: thesis: ( x < (h + c) . m & (h + c) . m < x + r )
consider m1 being Nat such that
A15: m = N + m1 by A14, 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 < ((h ^\ N) + c) . m1 & ((h ^\ N) + c) . m1 < x + r ) by A10, XXREAL_1:4;
hence ( x < (h + c) . m & (h + c) . m < x + r ) by A15, A11; :: thesis: verum

end;