let a, b, c be Complex; :: thesis: (a / b) / c = (1 / b) * (a / c)
(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 ;
hence (a / b) / c = (b ") * (a / c) by XCMPLX_0:def 9
.= (1 / b) * (a / c) by Lm4 ;
:: thesis: verum