let i1, i2 be Integer; :: thesis: ( i2 <> 0 implies i1 = ((i1 div i2) * i2) + (i1 mod i2) )
assume i2 <> 0 ; :: thesis: i1 = ((i1 div i2) * i2) + (i1 mod i2)
then ((i1 div i2) * i2) + (i1 mod i2) = ((i1 div i2) * i2) + (i1 - ((i1 div i2) * i2)) by Def10
.= i1 ;
hence i1 = ((i1 div i2) * i2) + (i1 mod i2) ; :: thesis: verum