theorem Th31: :: TAYLOR_1:31

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 + 1,Z holds
f is_differentiable_on n + 1,Z1