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