theorem Th13: :: HILB10_5:13

for n, k being Nat
for P being INT -valued Polynomial of k,F_Real
for a being Integer
for perm being Permutation of n
for i1 being Element of n st k <= n holds
{ p where p is b₁ -element XFinSequence of NAT : for q being b₂ -element XFinSequence of NAT st q = (p * perm) | k holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)