let a, b be complex number ; :: thesis: (a " ) / (b " ) = b / a
thus (a " ) / (b " ) = (a " ) * ((b " ) " ) by XCMPLX_0:def 9
.= b / a by XCMPLX_0:def 9 ; :: thesis: verum