let a, b, c be complex number ; :: thesis: (a / b) / c = (1 / c) * (a / b)
thus (a / b) / c = (c " ) * (a / b) by XCMPLX_0:def 9
.= (1 / c) * (a / b) by Lm4 ; :: thesis: verum