let c, a, b be complex number ; :: thesis: ( c <> 0 implies a / b = (a / c) * (c / b) )
assume A1: c <> 0 ; :: thesis: a / b = (a / c) * (c / b)
thus a / b = a * (b " ) by XCMPLX_0:def 9
.= ((a / c) * c) * (b " ) by A1, Lm3
.= (a / c) * (c * (b " ))
.= (a / c) * (c / b) by XCMPLX_0:def 9 ; :: thesis: verum