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