theorem :: EULER_2:13

for m being Nat
for F being FinSequence of NAT holds (F mod m) mod m = F mod m