theorem Th11: :: HILB10_5:12

for k, n1, n2, i, j, l, m, n being Nat
for i1, i2, i3, i4 being Element of n st n1 + n2 <= n holds
{ p where p is b₈ -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT)