ex r being Real st

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

then consider h being non-zero 0 -convergent Real_Sequence, c being constant Real_Sequence such that

A11: ( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) ) by Th1;

let g1, g2 be Real; :: 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

g1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( 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

g2 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) implies g1 = g2 )

assume that

A12: 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

g1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) and

A13: 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

g2 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ; :: thesis: g1 = g2

g1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A12, A11;

hence g1 = g2 by A13, A11; :: thesis: verum

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

then consider h being non-zero 0 -convergent Real_Sequence, c being constant Real_Sequence such that

A11: ( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) ) by Th1;

let g1, g2 be Real; :: 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

g1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( 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

g2 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) implies g1 = g2 )

assume that

A12: 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

g1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) and

A13: 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

g2 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ; :: thesis: g1 = g2

g1 = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A12, A11;

hence g1 = g2 by A13, A11; :: thesis: verum