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