theorem Th81: :: XCMPLX_1:81

for a, b, e being Complex holds a / (b / e) = e * (a / b)