let z, z1 be complex number ; :: 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 Th62
.= ((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