ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) by A1, Def3;
then consider h being convergent_to_0 Real_Sequence, c being V8() Real_Sequence such that
A2: ( rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) ) by Th2;
take lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ; :: thesis: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))
let h1 be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) holds
lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c)))
let c1 be V8() Real_Sequence; :: thesis: ( rng c1 = {x0} & rng (h1 + c1) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) implies lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) )
assume A3: ( rng c1 = {x0} & rng (h1 + c1) c= dom f & ( for n being Element of NAT holds h1 . n > 0 ) ) ; :: thesis: lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1)))
A4: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, Def3;
A5: {x0} c= dom f

proof

let x be set ; :: 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 A6: x = x0 by TARSKI:def 1;
consider r being Real such that
A7: ( r > 0 & [.x0,(x0 + r).] c= dom f ) by A1, Def3;
x0 + 0 <= x0 + r by A7, XREAL_1:9;
then x0 in [.x0,(x0 + r).] by XXREAL_1:1;
hence x in dom f by A6, A7; :: thesis: verum

end;

c1 = c by A2, A3, FDIFF_2:5;
hence lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) by A2, A3, A4, A5, Th4; :: thesis: verum