let z1, z2 be complex number ; :: thesis: exp (z1 + z2) = (exp z1) * (exp z2)
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 ;
hence exp (z1 + z2) = (exp z1) * (exp z2) ; :: thesis: verum