let a, b, c be Complex; :: thesis: a / (b / c) = (c / b) * a
a / (b / c) = (a * c) / b by Lm2
.= (a * c) * (b ") by XCMPLX_0:def 9
.= a * (c * (b "))
.= a * (c / b) by XCMPLX_0:def 9 ;
hence a / (b / c) = (c / b) * a ; :: thesis: verum