let f be Function of REAL,REAL; :: thesis: ( f is constant implies f is differentiable )
assume A1: f is constant ; :: thesis: f is differentiable
A2: dom f = REAL by FUNCT_2:def 1;
ex r being Element of REAL st rng f = {r} by A1, FUNCT_2:111;
hence f is differentiable by A2, Lm1, FDIFF_1:11; :: thesis: verum