for x being Real st x in REAL holds
diff (exp_R,x) = exp_R . x by SIN_COS:66;
hence exp_R `| REAL = exp_R by FDIFF_1:def 7, SIN_COS:47, SIN_COS:66; :: thesis: verum