let p, q be Real; (sin . (p + q)) - (sin . p) = (q * (cos . p)) + (q * (Re ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
(sin . (p + q)) - (sin . p) =
(sin . (p + q)) - (Im (Sum ((p * <i>) ExpSeq)))
by Def16
.=
(Im (Sum (((p + q) * <i>) ExpSeq))) - (Im (Sum ((p * <i>) ExpSeq)))
by Def16
.=
Im ((Sum (((p * <i>) + (q * <i>)) ExpSeq)) - (Sum ((p * <i>) ExpSeq)))
by COMPLEX1:19
.=
Im (((Sum ((p * <i>) ExpSeq)) * (q * <i>)) + (((q * <i>) * (Sum ((q * <i>) P_dt))) * (Sum ((p * <i>) ExpSeq))))
by Th58
.=
Im ((((cos . p) + ((sin . p) * <i>)) * (q * <i>)) + (((q * <i>) * (Sum ((q * <i>) P_dt))) * (Sum ((p * <i>) ExpSeq))))
by Lm3
.=
Im ((((cos . p) + ((sin . p) * <i>)) * (q * <i>)) + (((q * <i>) * (Sum ((q * <i>) P_dt))) * ((cos . p) + ((sin . p) * <i>))))
by Lm3
.=
(Im ((- (q * (sin . p))) + ((q * (cos . p)) * <i>))) + (Im (((q * <i>) * (Sum ((q * <i>) P_dt))) * ((cos . p) + ((sin . p) * <i>))))
by COMPLEX1:8
.=
(q * (cos . p)) + (Im ((q * <i>) * ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
by COMPLEX1:12
.=
(q * (cos . p)) + (q * (Re ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
by Lm12
;
hence
(sin . (p + q)) - (sin . p) = (q * (cos . p)) + (q * (Re ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
; verum