let a, b, c, d, e be complex number ; :: 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 Th82
.= (e / c) * (a / (b * d)) by Th82 ; :: thesis: verum