theorem Th16: :: HILB10_5:16

for n, k being Nat
for p being INT -valued Polynomial of ((2 + n) + k),F_Real
for X being b₁ -element XFinSequence of NAT
for x being Element of NAT holds
( ( for z being Element of NAT st z <= x holds
ex y being b₂ -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) iff ex Y being b₂ -element XFinSequence of NAT ex Z, e, K being Element of NAT st
( K > x & K >= (sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) & ( for i being Nat st i in k holds
Y . i > e ) & e > x & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) )