theorem :: XCMPLX_1:208

for a, b being Complex st a <> 0 & b <> 0 holds
(a ") * (b ") <> 0 ;