let z1, z2 be complex number ; :: thesis: exp (z1 + z2) = (exp z1) * (exp z2)
A1: exp (z1 + z2) = Sum ((z1 + z2) ExpSeq ) by Def18
.= (Sum (z1 ExpSeq )) * (Sum (z2 ExpSeq )) by Lm2
.= (exp z1) * (Sum (z2 ExpSeq )) by Def18
.= (exp z1) * (exp z2) by Def18 ;
thus exp (z1 + z2) = (exp z1) * (exp z2) by A1; :: thesis: verum