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 Lm7
.= (a / d) * (b / c) by Lm7 ; :: thesis: verum