theorem Th12: :: SIN_COS2:12

for p, q being Real holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)