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