theorem :: XCMPLX_1:204

for a, b being Complex holds (a ") * (b ") = (a * b) " by Lm1;