:: deftheorem Def6 defines diophantine HILB10_2:def 6 :
for n being Nat
for A being Subset of (n -xtuples_of NAT) holds
( A is diophantine iff ex m being Nat ex p being INT -valued Polynomial of (n + m),F_Real st
for s being object holds
( s in A iff ex x being b₁ -element XFinSequence of NAT ex y being b₃ -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) ) );