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