let g1, g2 be Real; :: 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
g1 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ) & ( 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
g2 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ) implies g1 = g2 )
assume A8: ( ( 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
g1 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ) & ( 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
g2 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ) ) ; :: thesis: g1 = g2
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
A9: ( rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) ) by Th2;
g1 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) by A8, A9;
hence g1 = g2 by A8, A9; :: thesis: verum