theorem Th25: :: HILB10_4:25

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