let a, b, c be complex number ; :: 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