theorem :: HILB10_4:33

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