let a, b, c, d, n be Integer; :: thesis: (((a + b) + c) + d) mod n = ((((a mod n) + (b mod n)) + (c mod n)) + (d mod n)) mod n
thus (((a + b) + c) + d) mod n = ((((a + b) + c) mod n) + (d mod n)) mod n by NAT_D:66
.= (((((a mod n) + (b mod n)) + (c mod n)) mod n) + ((d mod n) mod n)) mod n by Th8
.= ((((a mod n) + (b mod n)) + (c mod n)) + (d mod n)) mod n by NAT_D:66 ; :: thesis: verum