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 )))
A1: (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 ))) ;
thus (Sum ((z1 + z) ExpSeq )) - (Sum (z1 ExpSeq )) = ((Sum (z1 ExpSeq )) * z) + ((z * (Sum (z P_dt ))) * (Sum (z1 ExpSeq ))) by A1; :: thesis: verum