theorem Th31: :: HILB10_4:31

for n being Nat
for i1, i2 being Element of n st n <> 0 holds
{ p where p is b₁ -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)