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