theorem Th8: :: INT_5:8

for n being Nat
for p being Prime
for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds
for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n