theorem Th15: :: HILB10_5:15

for k being Nat
for P being INT -valued Polynomial of (k + 1),F_Real
for n being Nat
for i1, i2 being Element of n st k + 1 <= n & k in i1 holds
{ p where p is b₃ -element XFinSequence of NAT : for q being b₁ + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds
eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)