let a, b, c, d, e be Complex; :: thesis: a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))
thus a / ((b * c) * (d / e)) = a / ((b * c) * (d * (e "))) by XCMPLX_0:def 9
.= a / (c * ((b * d) * (e ")))
.= a / (c * ((b * d) / e)) by XCMPLX_0:def 9
.= a / ((b * d) / (e / c)) by Th81
.= (e / c) * (a / (b * d)) by Th81 ; :: thesis: verum