let h be Function of REAL,REAL; :: thesis: ( h = r + f implies h is differentiable )
reconsider r = r as Element of REAL by XREAL_0:def 1;
reconsider g = REAL --> r as differentiable Function of REAL,REAL ;
dom f = REAL by FUNCT_2:def 1;
then g + f = r + f by Th3;
hence ( h = r + f implies h is differentiable ) ; :: thesis: verum