theorem Th11: :: HILB10_3:11

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