theorem Th30: :: TAYLOR_1:30

for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n