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