theorem Th1: :: HILB10_5:1

for n, k being Nat
for p being INT -valued Polynomial of n,F_Real
for x, y being b₁ -element XFinSequence of NAT st k <> 0 & ( for i being Nat st i in n holds
k divides (x . i) - (y . i) ) holds
k divides (eval (p,(@ x))) - (eval (p,(@ y)))