let f be Function of REAL,REAL; :: thesis: ( f = id REAL implies f is differentiable )
assume f = id REAL ; :: thesis: f is differentiable
then f is_differentiable_on REAL by Lm1, FDIFF_1:17;
hence f is differentiable by FUNCT_2:def 1; :: thesis: verum