let z, z1 be Complex; :: thesis: (Sum ((z1 + z) ExpSeq)) - (Sum (z1 ExpSeq)) = ((Sum (z1 ExpSeq)) * z) + ((z * (Sum (z P_dt))) * (Sum (z1 ExpSeq)))
(Sum ((z1 + z) ExpSeq)) - (Sum (z1 ExpSeq)) = ((Sum (z1 ExpSeq)) * (Sum (z ExpSeq))) - ((Sum (z1 ExpSeq)) * 1r) by Lm2
.= (Sum (z1 ExpSeq)) * ((((Sum (z ExpSeq)) - 1r) - z) + z)
.= (Sum (z1 ExpSeq)) * ((z * (Sum (z P_dt))) + z) by Th56
.= ((Sum (z1 ExpSeq)) * z) + ((z * (Sum (z P_dt))) * (Sum (z1 ExpSeq))) ;
hence (Sum ((z1 + z) ExpSeq)) - (Sum (z1 ExpSeq)) = ((Sum (z1 ExpSeq)) * z) + ((z * (Sum (z P_dt))) * (Sum (z1 ExpSeq))) ; :: thesis: verum