let a, b, c be complex number ; :: thesis: a * (b / c) = (a * b) / c
thus a * (b / c) = (a / 1) * (b / c)
.= (a * b) / (1 * c) by Lm7
.= (a * b) / c ; :: thesis: verum