let a be non zero Integer; :: thesis: for b being Integer holds (a * b) mod a = 0
let b be Integer; :: thesis: (a * b) mod a = 0
(a * b) mod a = (a * b) - (((a * b) div a) * a) by Def10
.= 0 ;
hence (a * b) mod a = 0 ; :: thesis: verum