theorem :: HILB10_5:18

for n, k being Nat
for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is b₁ -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being b₂ -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } is diophantine Subset of (n -xtuples_of NAT)