let a, b, d, e be Real; :: thesis: (a / b) / (d / e) = (a / d) * (e / b)
thus (a / b) / (d / e) = (a * e) / (b * d) by XCMPLX_1:84
.= (a / d) * (e / b) by XCMPLX_1:76 ; :: thesis: verum