theorem :: HILB10_4:27

for n being Nat
for A being diophantine Subset of (n -xtuples_of NAT)
for k, nk being Nat st k + nk = n holds
{ (p /^ nk) where p is b₁ -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)