let a, c, b, d be complex number ; :: 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