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