theorem Th24: :: TAYLOR_1:24

for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for n being Nat st f is_differentiable_on n,Z holds
for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n