theorem :: XCMPLX_1:111
for a, b being Complex st a <> 0 & b <> 0 holds
1 / (a * b) <> 0 ;