theorem Th61: :: SIN_COS:62

for p, q being Real holds (exp_R . (p + q)) - (exp_R . p) = (q * (exp_R . p)) + ((q * (exp_R . p)) * (Re (Sum (q P_dt))))