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