theorem Th2: :: HILB10_6:2

for n being Nat
for i, j being Element of n holds { p where p is b₁ -element XFinSequence of NAT : p . i = (((p . j) -' 1) !) + 1 } is diophantine Subset of (n -xtuples_of NAT)