:: deftheorem defines differentiable POLYDIFF:def 2 :
for f being Function of REAL,REAL holds
( f is differentiable iff for r being Real holds f is_differentiable_in r );