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