let i be Integer; :: thesis: i div 0 = 0
A1: i / 0 = i * (0 ") by XCMPLX_0:def 9
.= i * 0 ;
0 - 1 < 0 ;
hence i div 0 = 0 by A1, Def6; :: thesis: verum