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