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 Th47
.= (Re (Sum ((p + q) ExpSeq))) - (Re (Sum (p ExpSeq))) by Th47
.= Re ((Sum ((p + q) ExpSeq)) - (Sum (p ExpSeq))) by COMPLEX1:19
.= Re (((Sum (p ExpSeq)) * q) + ((q * (Sum (q P_dt))) * (Sum (p ExpSeq)))) by Th58
.= (Re ((Sum (p ExpSeq)) * q)) + (Re ((q * (Sum (q P_dt))) * (Sum (p ExpSeq)))) by COMPLEX1:8
.= (q * (Re (Sum (p ExpSeq)))) + (Re ((q * (Sum (q P_dt))) * (Sum (p ExpSeq)))) by Lm12
.= (q * (exp_R . p)) + (Re (q * ((Sum (q P_dt)) * (Sum (p ExpSeq))))) by Th47
.= (q * (exp_R . p)) + (q * (Re ((Sum (q P_dt)) * (Sum (p ExpSeq))))) by Lm12
.= (q * (exp_R . p)) + (q * (Re ((Sum (q P_dt)) * (Sum (p rExpSeq))))) by Lm9
.= (q * (exp_R . p)) + (q * (Re ((Sum (q P_dt)) * ((exp_R . p) + (0 * <i>))))) by Def22
.= (q * (exp_R . p)) + (q * ((exp_R . p) * (Re (Sum (q P_dt))))) by Lm12
.= (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