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