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