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