let p, q be Real; :: thesis: (exp_R . (p + q)) - (exp_R . p) = (q * (exp_R . p)) + ((q * (exp_R . p)) * (Re (Sum (q P_dt ))))
(exp_R . (p + q)) - (exp_R . p) = (exp_R . (p + q)) - (Re (Sum (p ExpSeq ))) by Th53
.= (Re (Sum ((p + q) ExpSeq ))) - (Re (Sum (p ExpSeq ))) by Th53
.= Re ((Sum ((p + q) ExpSeq )) - (Sum (p ExpSeq ))) by COMPLEX1:48
.= Re (((Sum (p ExpSeq )) * q) + ((q * (Sum (q P_dt ))) * (Sum (p ExpSeq )))) by Th64
.= (Re ((Sum (p ExpSeq )) * q)) + (Re ((q * (Sum (q P_dt ))) * (Sum (p ExpSeq )))) by COMPLEX1:19
.= (q * (Re (Sum (p ExpSeq )))) + (Re ((q * (Sum (q P_dt ))) * (Sum (p ExpSeq )))) by Lm17
.= (q * (exp_R . p)) + (Re (q * ((Sum (q P_dt )) * (Sum (p ExpSeq ))))) by Th53
.= (q * (exp_R . p)) + (q * (Re ((Sum (q P_dt )) * (Sum (p ExpSeq ))))) by Lm17
.= (q * (exp_R . p)) + (q * (Re ((Sum (q P_dt )) * (Sum (p rExpSeq ))))) by Lm14
.= (q * (exp_R . p)) + (q * (Re ((Sum (q P_dt )) * ((exp_R . p) + (0 * <i> ))))) by Def26
.= (q * (exp_R . p)) + (q * ((exp_R . p) * (Re (Sum (q P_dt ))))) by Lm17
.= (q * (exp_R . p)) + ((q * (exp_R . p)) * (Re (Sum (q P_dt )))) ;
hence (exp_R . (p + q)) - (exp_R . p) = (q * (exp_R . p)) + ((q * (exp_R . p)) * (Re (Sum (q P_dt )))) ; :: thesis: verum