theorem :: XCMPLX_1:216

for a being Complex holds 1 / (a ") = a by Lm16;