theorem :: XCMPLX_1:217

for a being Complex holds (1 / a) " = a