theorem :: HILB10_4:38

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