theorem :: XCMPLX_1:73

for a, b being Complex st a * b = 1 holds
a = 1 / b