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