:: deftheorem defines is_differentiable_on FDIFF_1:def 6 :
for f being PartFunc of REAL,REAL
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) );