theorem Th3: :: NUMERAL1:3

for d, e being XFinSequence of NAT
for n being Nat 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