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