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
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) } is diophantine Subset of (n -xtuples_of NAT)