theorem Th14: :: HILB10_5:14

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