:: deftheorem defines is_differentiable_on TAYLOR_1:def 6 :
for f being PartFunc of REAL,REAL
for n being Nat
for Z being Subset of REAL holds
( f is_differentiable_on n,Z iff for i being Nat st i <= n - 1 holds
(diff (f,Z)) . i is_differentiable_on Z );