let z1, z2 be complex number ; :: thesis: (z1 / z2) *' = (z1 *' ) / (z2 *' )
thus (z1 / z2) *' = (z1 * (z2 " )) *' by XCMPLX_0:def 9
.= (z1 *' ) * ((z2 " ) *' ) by Th121
.= (z1 *' ) * ((z2 *' ) " ) by Th122
.= (z1 *' ) / (z2 *' ) by XCMPLX_0:def 9 ; :: thesis: verum