let a, b, e be complex number ; :: thesis: (a / b) * e = (e / b) * a
thus (a / b) * e = (a * e) / b by Lm9
.= (e / b) * a by Lm9 ; :: thesis: verum