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