theorem :: SIN_COS:49

for th being Real holds exp th = exp_R th