let a, b be Complex; :: thesis: (a ") / b = (a * b) "
thus (a ") / b = (a ") * (b ") by XCMPLX_0:def 9
.= (a * b) " by Lm1 ; :: thesis: verum