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