theorem :: XCMPLX_1:205

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