let a be Complex; :: thesis: 1 / a = a "
thus 1 / a = 1 * (a ") by XCMPLX_0:def 9
.= a " ; :: thesis: verum