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