for x being Real st x in REAL holds
diff exp_R ,x = exp_R . x by SIN_COS:71;
hence exp_R `| REAL = exp_R by FDIFF_1:def 8, SIN_COS:51, SIN_COS:71; :: thesis: verum