let i, j, k, l be Integer; :: thesis: ( i mod l = j mod l implies (k + i) mod l = (k + j) mod l )
assume A1: i mod l = j mod l ; :: thesis: (k + i) mod l = (k + j) mod l
thus (k + i) mod l = ((k mod l) + (i mod l)) mod l by NAT_D:66
.= (k + j) mod l by A1, NAT_D:66 ; :: thesis: verum