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