theorem Th59: :: SIN_COS:60

for p, q being Real holds (cos . (p + q)) - (cos . p) = (- (q * (sin . p))) - (q * (Im ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))