theorem :: XCMPLX_1:54

for a, b being Complex st a / b <> 0 holds
b = a / (a / b)