A2: {x0} c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {x0} ; :: thesis:
then A3: x = x0 by TARSKI:def 1;
consider r being Real such that
A4: r > 0 and
A5: [.x0,(x0 + r).] c= dom f by A1;
x0 + 0 <= x0 + r by A4, XREAL_1:7;
then x0 in [.x0,(x0 + r).] by XXREAL_1:1;
hence x in dom f by A3, A5; :: thesis:

end;

A6: 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
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1;
ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) by A1;
then consider h being non-zero 0 -convergent Real_Sequence, c being constant Real_Sequence such that
A7: rng c = {x0} and
A8: ( rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) ) by Th2;
take lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ; :: thesis:
let h1 be non-zero 0 -convergent Real_Sequence; :: thesis:
let c1 be constant Real_Sequence; :: thesis:
assume that
A9: rng c1 = {x0} and
A10: ( rng (h1 + c1) c= dom f & ( for n being Nat holds h1 . n > 0 ) ) ; :: thesis:
c1 = c by A7, A9, FDIFF_2:5;
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) by A7, A8, A10, A6, A2, Th4; :: thesis: