A1: dom exp_R = REAL by SIN_COS:51;
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 A1, FDIFF_1:def 8, SIN_COS:71; :: thesis: verum