for f being Function of REAL,REAL holds
( f is differentiable iff for r being Real holds f is_differentiable_in r )