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