let th be real number ; :: thesis: ( exp_R is_differentiable_on REAL & diff exp_R ,th = exp_R . th )
( [#] REAL is open Subset of REAL & REAL c= dom exp_R & ( for r being Real st r in REAL holds
exp_R is_differentiable_in r ) ) by Th70, FUNCT_2:def 1;
hence ( exp_R is_differentiable_on REAL & diff exp_R ,th = exp_R . th ) by Th70, FDIFF_1:16; :: thesis: verum