let i, j be Nat; :: thesis: (j + j) mod j = 0
thus (j + j) mod j = (2 * j) mod j
.= 0 by NAT_D:13 ; :: thesis: verum