theorem :: XCMPLX_1:60

for a being Complex st a <> 0 holds
a / a = 1 by Lm5;