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