theorem Th5: :: HILB10_3:5

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