theorem :: SIN_COS:23

for z1, z2 being Complex holds exp (z1 + z2) = (exp z1) * (exp z2)