let a, b be Integer; :: thesis: for n being Nat st n > 0 holds
((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n
let n be Nat; :: thesis: ( n > 0 implies ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n )
assume n > 0 ; :: thesis: ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n
then (a mod n) + ((a div n) * n) = (a - ((a div n) * n)) + ((a div n) * n) by INT_1:def 10
.= a + 0 ;
then n divides (a + (b mod n)) - ((a mod n) + (b mod n)) by INT_1:def 3;
then a + (b mod n),(a mod n) + (b mod n) are_congruent_mod n by INT_2:15;
hence ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n by NAT_D:64; :: thesis: verum