let a, b, e be complex number ; :: thesis: a / (b / e) = e * (a / b)
thus a / (b / e) = (a * e) / b by Lm2
.= (e * a) * (b " ) by XCMPLX_0:def 9
.= e * (a * (b " ))
.= e * (a / b) by XCMPLX_0:def 9 ; :: thesis: verum