let i, j, n, k be Element of NAT ; :: thesis: ADD_MOD (ADD_MOD i,j,n),k,n = ADD_MOD i,(ADD_MOD j,k,n),n
thus ADD_MOD (ADD_MOD i,j,n),k,n = ((i + j) + k) mod (2 to_power n) by NAT_D:23
.= (i + (j + k)) mod (2 to_power n)
.= ADD_MOD i,(ADD_MOD j,k,n),n by NAT_D:22 ; :: thesis: verum