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