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