theorem :: HILB10_4:39

for i, n1, n2, n being Nat
for i1 being Element of n holds { p where p is b₄ -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)