theorem Th14: :: HILB10_3:14

for n being Nat
for a being Integer
for i1 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)