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