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