theorem :: NUMERAL2:17

for d, e being XFinSequence of INT
for n being Integer st dom d = dom e & ( for i being Nat st i in dom d holds
e . i = (d . i) mod n ) holds
(Sum d) mod n = (Sum e) mod n