theorem :: XCMPLX_1:96
for a, b, c, d being Complex st c <> 0 & d <> 0 & a * c = b / d holds
a * d = b / c