theorem Th23: :: HILB10_3:23

for n being Nat
for i1, i2, i3 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of (n -xtuples_of NAT)