theorem :: NUMBER01:17

for s being FinSequence of NAT
for n being Nat st n > 1 & len s = n - 1 & ( for i being Nat st i in dom s holds
s . i = i |^ n ) & n is odd holds
n divides Sum s