:: deftheorem Def8 defines differentiable FDIFF_1:def 8 :
for f being PartFunc of REAL,REAL holds
( f is differentiable iff f is_differentiable_on dom f );