let f be Function of REAL,REAL; :: thesis: ( f is differentiable iff for r being Real holds f is_differentiable_in r )
A1: f | REAL = f ;
dom f = REAL by FUNCT_2:def 1;
hence ( f is differentiable implies for r being Real holds f is_differentiable_in r ) by A1, FDIFF_1:def 6, XREAL_0:def 1; :: thesis: ( ( for r being Real holds f is_differentiable_in r ) implies f is differentiable )
assume for r being Real holds f is_differentiable_in r ; :: thesis: f is differentiable
hence f is_differentiable_on dom f ; :: according to FDIFF_1:def 8 :: thesis: verum