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 Th5;
hence ( h = r (#) f implies h is differentiable ) ; :: thesis: verum