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