let z1, z2 be Complex; :: thesis: (z1 / z2) *' = (z1 *') / (z2 *')
thus (z1 / z2) *' = (z1 * (z2 ")) *' by XCMPLX_0:def 9
.= (z1 *') * ((z2 ") *') by Th35
.= (z1 *') * ((z2 *') ") by Th36
.= (z1 *') / (z2 *') by XCMPLX_0:def 9 ; :: thesis: verum