theorem Th1: :: HILB10_1:1

for n being Nat
for F being FinSequence of NAT st ( for k being Nat st 1 < k & k <= len F holds
(F . k) mod n = 0 ) holds
(Sum F) mod n = (F . 1) mod n