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