let a, b, e be Complex; :: thesis: (a / b) * e = (e / b) * a
thus (a / b) * e = (a * e) / b by Lm8
.= (e / b) * a by Lm8 ; :: thesis: verum