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