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