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