theorem :: XCMPLX_1:209

for a, b being Complex st a * (b ") = 1 holds
a = b