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