theorem :: XCMPLX_1:56

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