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