theorem Th60: :: SIN_COS:61

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