A2:
{x0} c= dom f

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1;

ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) by A1;

then consider h1 being non-zero 0 -convergent Real_Sequence, c1 being constant Real_Sequence such that

A7: rng c1 = {x0} and

A8: ( rng (h1 + c1) c= dom f & ( for n being Nat holds h1 . n < 0 ) ) by Th1;

take lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) ; :: thesis: for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) implies lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

assume that

A9: rng c = {x0} and

A10: ( rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) ) ; :: thesis: lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

c1 = c by A7, A9, FDIFF_2:5;

hence lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A7, A8, A2, A10, A6, Th3; :: thesis: verum

proof

A6:
for h being non-zero 0 -convergent Real_Sequence
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in dom f )

assume x in {x0} ; :: thesis: x in dom f

then A3: x = x0 by TARSKI:def 1;

consider r being Real such that

A4: r > 0 and

A5: [.(x0 - r),x0.] c= dom f by A1;

x0 - r <= x0 by A4, XREAL_1:44;

then x0 in [.(x0 - r),x0.] by XXREAL_1:1;

hence x in dom f by A3, A5; :: thesis: verum

end;assume x in {x0} ; :: thesis: x in dom f

then A3: x = x0 by TARSKI:def 1;

consider r being Real such that

A4: r > 0 and

A5: [.(x0 - r),x0.] c= dom f by A1;

x0 - r <= x0 by A4, XREAL_1:44;

then x0 in [.(x0 - r),x0.] by XXREAL_1:1;

hence x in dom f by A3, A5; :: thesis: verum

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1;

ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) by A1;

then consider h1 being non-zero 0 -convergent Real_Sequence, c1 being constant Real_Sequence such that

A7: rng c1 = {x0} and

A8: ( rng (h1 + c1) c= dom f & ( for n being Nat holds h1 . n < 0 ) ) by Th1;

take lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) ; :: thesis: for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) implies lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )

assume that

A9: rng c = {x0} and

A10: ( rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) ) ; :: thesis: lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

c1 = c by A7, A9, FDIFF_2:5;

hence lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A7, A8, A2, A10, A6, Th3; :: thesis: verum