theorem Th22: :: CFDIFF_1:22

for f being PartFunc of COMPLEX,COMPLEX
for x0 being Complex
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Complex_Sequence
for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )