let i be Integer; :: thesis: i div 0 = 0
i / 0 = i * (0 ") by XCMPLX_0:def 9
.= i * 0 ;
hence i div 0 = 0 ; :: thesis: verum