theorem :: SIN_COS:50

for p, q being Real holds exp_R (p + q) = (exp_R p) * (exp_R q) by Lm10;