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