let z1, z2 be Complex; :: thesis: exp (z1 + z2) = (exp z1) * (exp z2)
exp (z1 + z2) = Sum ((z1 + z2) ExpSeq) by Def14
.= (Sum (z1 ExpSeq)) * (Sum (z2 ExpSeq)) by Lm2
.= (exp z1) * (Sum (z2 ExpSeq)) by Def14
.= (exp z1) * (exp z2) by Def14 ;
hence exp (z1 + z2) = (exp z1) * (exp z2) ; :: thesis: verum