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