let n, k be Nat; :: thesis:
let p be INT -valued Polynomial of ((2 + n) + k),F_Real; :: thesis:
let X be n -element XFinSequence of NAT ; :: thesis:
let x be Element of NAT ; :: thesis:
set x1 = x + 1;
thus ( ( for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) implies ex Y being k -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 !)) ) ) ) :: thesis:

assume A1: for z being Element of NAT st z <= x holds
ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ; :: thesis:
defpred S₁[ object , object ] means ( $1 in NAT & $2 is k -element XFinSequence of NAT & ( for z being Element of NAT
for y being k -element XFinSequence of NAT st z = $1 & y = $2 holds
eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) );
A2: for i being Nat st i in x + 1 holds
ex g being object st S₁[i,g]

let i be Nat; :: thesis:
assume i in x + 1 ; :: thesis:
then A3: i in Segm (x + 1) ;
reconsider z = i as Element of NAT by ORDINAL1:def 12;
i < x + 1 by A3, NAT_1:44;
then i <= x by NAT_1:13;
then consider y being k -element XFinSequence of NAT such that
A4: eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 by A1;
take y ; :: thesis:
thus S₁[i,y] by A4, ORDINAL1:def 12; :: thesis:

end;

consider YY being XFinSequence such that
A5: ( dom YY = x + 1 & ( for i being Nat st i in x + 1 holds
S₁[i,YY . i] ) ) from AFINSQ_1:sch 1(A2);
YY is XFinSequence-yielding by A5;
then reconsider YY = YY as XFinSequence-yielding XFinSequence ;
defpred S₂[ object , object ] means verum;
set M = { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ;
A6: { ((YY . i) . j) where i, j is Nat : S₂[i,j] } is finite from HILB10_5:sch 1();
A7: { ((YY . i) . j) where i, j is Nat : S₂[i,j] } is natural-membered

proof

let x be object ; :: according to MEMBERED:def 6 :: thesis:
assume x in { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ; :: thesis:
then consider i, j being Nat such that
A8: ( x = (YY . i) . j & S₂[i,j] ) ;

per cases ;

suppose i in dom YY ; :: thesis:

then S₁[i,YY . i] by A5;
hence x is natural by A8; :: thesis:

end;

suppose not i in dom YY ; :: thesis:

then YY . i = {} by FUNCT_1:def 2;
hence x is natural by A8; :: thesis:

end;

then reconsider Mx = { ((YY . i) . j) where i, j is Nat : S₂[i,j] } \/ {x,1} as non empty finite natural-membered set by A6;
set e = 1 + (max Mx);
set K = ((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)));
set h = 1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)));
A9: len (1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)))) = x + 1 by CARD_1:def 7;
A10: for i being Nat st i in dom (1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)))) holds
(1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)))) . i = (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * i) + 1

proof

let i be Nat; :: thesis:
assume A11: i in dom (1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)))) ; :: thesis:
A12: ( dom (1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)))) = dom (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1))) & dom (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1))) = dom (idseq (x + 1)) ) by VALUED_1:def 2, VALUED_1:def 5;
thus (1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)))) . i = 1 + ((((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1))) . i) by A11, VALUED_1:def 2
.= 1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * ((idseq (x + 1)) . i)) by A11, A12, VALUED_1:def 5
.= (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * i) + 1 by A11, A12, FINSEQ_2:49 ; :: thesis:

end;

A13: ( (x + 1) + (1 + (max Mx)) <= ((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p))) & x + 1 <= (x + 1) + (1 + (max Mx)) & 1 + (max Mx) <= (x + 1) + (1 + (max Mx)) ) by NAT_1:11;
then A14: ( ((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p))) >= x + 1 & x + 1 > 0 ) by XXREAL_0:2;
then reconsider h = 1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1))) as CR_Sequence by Th2;
rng h c= NAT by VALUED_0:def 6;
then A15: h is FinSequence of NAT by FINSEQ_1:def 4;
0 + 1 <= x + 1 by NAT_1:13;
then ( h . 1 divides Product h & h . 1 = (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * 1) + 1 ) by A10, A15, INT_4:32, A9, FINSEQ_3:25;
then ( h . 1 <= Product h & h . 1 > (((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) ! ) by INT_2:27, NAT_1:13;
then ( ((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p))) <= (((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) ! & (((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) ! < Product h ) by XXREAL_0:2, NEWTON:38;
then ( 1 + (max Mx) <= ((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p))) & ((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p))) < Product h ) by A13, XXREAL_0:2;
then A16: 1 + (max Mx) < Product h by XXREAL_0:2;
defpred S₃[ object , object ] means ( $1 in NAT & $2 in NAT & ( for i, z being Nat st i = $1 & z = $2 holds
( 1 + (max Mx) < z & ( for j, F being Nat st j in x + 1 & F = (YY . j) . i holds
z,F are_congruent_mod h . (j + 1) ) ) ) );
A17: for i being Nat st i in k holds
ex Y being object st S₃[i,Y]

proof

let i be Nat; :: thesis:
assume i in k ; :: thesis:
deffunc H₁( Nat) -> set = (YY . ($1 -' 1)) . i;
consider X being FinSequence such that
A18: ( len X = x + 1 & ( for k being Nat st k in dom X holds
X . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng X c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng X ; :: thesis:
then consider x being object such that
A19: ( x in dom X & X . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A19;
X . x = (YY . (x -' 1)) . i by A18, A19;
then X . x in { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ;
then X . x is natural by A7;
hence y in NAT by A19; :: thesis:

end;

then reconsider X = X as FinSequence of NAT by FINSEQ_1:def 4;
consider z being Integer such that
A20: ( 0 <= z & z < Product h ) and
A21: for i being Nat st i in dom X holds
z,X . i are_congruent_mod h . i by INT_6:41, A18, A9;
take Y = z + (Product h); :: thesis:
thus ( i in NAT & Y in NAT ) by A20, ORDINAL1:def 12; :: thesis:
let I, Z be Nat; :: thesis:
assume A22: ( I = i & Z = Y ) ; :: thesis:
Y >= Product h by A20, NAT_1:11;
hence 1 + (max Mx) < Z by A22, A16, XXREAL_0:2; :: thesis:
let j, F be Nat; :: thesis:
assume A23: ( j in x + 1 & F = (YY . j) . I ) ; :: thesis:
x + 1 = Segm (x + 1) ;
then j < x + 1 by A23, NAT_1:44;
then A24: ( 1 <= j + 1 & j + 1 <= x + 1 ) by NAT_1:11, NAT_1:13;
then A25: z,X . (j + 1) are_congruent_mod h . (j + 1) by A21, A18, FINSEQ_3:25;
j + 1 in dom h by A24, A9, FINSEQ_3:25;
then h . (j + 1) divides (Product h) - 0 by A15, INT_4:32;
then Product h, 0 are_congruent_mod h . (j + 1) by INT_1:def 4;
then A26: Y,(X . (j + 1)) + 0 are_congruent_mod h . (j + 1) by A25, INT_1:16;
X . (j + 1) = (YY . ((j + 1) -' 1)) . i by A18, A24, FINSEQ_3:25;
hence Z,F are_congruent_mod h . (j + 1) by A26, A23, A22, NAT_D:34; :: thesis:

end;

consider YC being XFinSequence such that
A27: ( dom YC = k & ( for i being Nat st i in k holds
S₃[i,YC . i] ) ) from AFINSQ_1:sch 1(A17);
rng YC c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng YC ; :: thesis:
then ex x being object st
( x in dom YC & YC . x = y ) by FUNCT_1:def 3;
hence y in NAT by A27; :: thesis:

end;

then reconsider YC = YC as k -element XFinSequence of NAT by A27, CARD_1:def 7, RELAT_1:def 19;
consider Z being Nat such that
A29: ( Product (1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * (idseq (x + 1)))) = 1 + (((((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p)))) !) * Z) & ( x + 1 > 0 implies Z > 0 ) ) by Lm1;
reconsider Z1 = Z - 1 as Element of NAT by NAT_1:20, A29;
reconsider e = 1 + (max Mx), K = ((x + 1) + (1 + (max Mx))) + ((sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * (1 + (max Mx))) |^ (degree p))) as Element of NAT by ORDINAL1:def 12;
take YC ; :: thesis:
take Z1 ; :: thesis:
take e ; :: thesis:
take K ; :: thesis:
thus ( K > x & K >= (sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) ) by NAT_1:11, A14, NAT_1:13; :: thesis:
thus for i being Nat st i in k holds
YC . i > e by A27; :: thesis:
x in {x,1} by TARSKI:def 2;
then x in Mx by XBOOLE_0:def 3;
then x <= max Mx by XXREAL_2:def 8;
hence x < e by NAT_1:13; :: thesis:
thus 1 + ((Z1 + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) by A29; :: thesis:
A30: for b, c being Element of NAT st b in dom h & c in dom h & b <> c holds
(h . b) gcd (h . c) = 1 by INT_2:def 3, INT_6:def 2;
reconsider E = eval (p,(@ ((<%Z1,x%> ^ X) ^ YC))) as Integer ;
A31: for b being Element of NAT st b in dom h holds
h . b divides E

proof

let b be Element of NAT ; :: thesis:
assume A32: b in dom h ; :: thesis:
A33: h . b = ((K !) * b) + 1 by A32, A10;
( 1 <= b & b <= x + 1 ) by A9, A32, FINSEQ_3:25;
then reconsider b1 = b - 1 as Element of NAT by NAT_1:21;
b1 + 1 <= x + 1 by A9, A32, FINSEQ_3:25;
then b1 < Segm (x + 1) by NAT_1:13;
then A34: b1 in x + 1 by NAT_1:44;
then reconsider YYb = YY . b1 as k -element XFinSequence of NAT by A5;
A35: eval (p,(@ ((<%b1,x%> ^ X) ^ YYb))) = 0 by A34, A5;
for i being Nat st i in (2 + n) + k holds
h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i)

proof

let i be Nat; :: thesis:
A36: len ((<%Z1,x%> ^ X) ^ YC) = (2 + n) + k by CARD_1:def 7;
A37: ( len <%Z1,x%> = 1 + 1 & len <%b1,x%> = 1 + 1 ) by CARD_1:def 7;
A38: ( len (<%Z1,x%> ^ X) = (len <%Z1,x%>) + (len X) & len (<%b1,x%> ^ X) = (len <%b1,x%>) + (len X) ) by AFINSQ_1:17;
A39: ( len YC = k & k = len YYb ) by CARD_1:def 7;
assume i in (2 + n) + k ; :: thesis:

per cases by A36, AFINSQ_1:20;

suppose A40: i in dom (<%Z1,x%> ^ X) ; :: thesis:

then A41: ( ((<%Z1,x%> ^ X) ^ YC) . i = (<%Z1,x%> ^ X) . i & ((<%b1,x%> ^ X) ^ YYb) . i = (<%b1,x%> ^ X) . i ) by A38, A37, AFINSQ_1:def 3;

per cases by A40, AFINSQ_1:20;

suppose A42: i in dom <%Z1,x%> ; :: thesis:

then A43: i in Segm 2 by CARD_1:def 7;
A44: ( (<%Z1,x%> ^ X) . i = <%Z1,x%> . i & (<%b1,x%> ^ X) . i = <%b1,x%> . i ) by A42, A37, AFINSQ_1:def 3;

per cases by A43, NAT_1:23, NAT_1:44;

suppose i = 0 ; :: thesis:

then A45: ( ((<%Z1,x%> ^ X) ^ YC) . i = Z1 & ((<%b1,x%> ^ X) ^ YYb) . i = b1 ) by A40, A38, A37, AFINSQ_1:def 3, A44;
A46: ((K !) + 1) gcd (K !) = ((b1 * (K !)) + ((K !) + 1)) gcd (K !) by EULER_1:8;
A47: ((K !) + 1) gcd (K !) = 1 by INT_2:def 3, PEPIN:1;
A48: h . b divides Product h by A15, A32, INT_4:32;
A49: (Z1 - b1) * (K !) = (Product (1 + ((K !) * (idseq (x + 1))))) - (h . b) by A29, A33;
h . b divides (Z1 - b1) * (K !) by A48, A49, INT_5:1;
hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by A45, A47, A46, INT_2:def 3, A33, INT_2:25; :: thesis:

end;

suppose i = 1 ; :: thesis:

hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by INT_2:12, A41, A44; :: thesis:

end;

suppose ex j being Nat st
( j in dom X & i = (len <%Z1,x%>) + j ) ; :: thesis:

then consider j being Nat such that
A50: ( j in dom X & i = 2 + j ) by A37;
( (<%Z1,x%> ^ X) . i = X . j & (<%b1,x%> ^ X) . i = X . j ) by A37, A50, AFINSQ_1:def 3;
hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by A41, INT_2:12; :: thesis:

end;

suppose ex j being Nat st
( j in dom YC & i = (len (<%Z1,x%> ^ X)) + j ) ; :: thesis:

then consider j being Nat such that
A51: ( j in dom YC & i = (len (<%Z1,x%> ^ X)) + j ) ;
A52: ((<%Z1,x%> ^ X) ^ YC) . i = YC . j by A51, AFINSQ_1:def 3;
A53: ((<%b1,x%> ^ X) ^ YYb) . i = YYb . j by A39, A37, A38, A51, AFINSQ_1:def 3;
reconsider J = j, YCj = YC . j as Element of NAT by A51;
YC . j,YYb . j are_congruent_mod h . (b1 + 1) by A34, A27, A51;
hence h . b divides (((<%Z1,x%> ^ X) ^ YC) . i) - (((<%b1,x%> ^ X) ^ YYb) . i) by A52, A53, INT_1:def 4; :: thesis:

end;

then h . b divides E - 0 by A32, A35, Th1;
hence h . b divides E ; :: thesis:

end;

Product h divides E

proof

per cases ;

suppose E >= 0 ; :: thesis:

hence Product h divides E by A30, A31, A15, INT_4:38; :: thesis:

end;

suppose E < 0 ; :: thesis:

then reconsider mE = - E as Element of NAT by INT_1:3;
for b being Element of NAT st b in dom h holds
h . b divides mE by A31, INT_2:10;
hence Product h divides E by INT_2:10, A30, A15, INT_4:38; :: thesis:

end;

then Product h divides E - 0 ;
hence eval (p,(@ ((<%Z1,x%> ^ X) ^ YC))), 0 are_congruent_mod 1 + ((Z1 + 1) * (K !)) by A29, INT_1:def 4; :: thesis:
let i be Nat; :: thesis:
assume A54: i in k ; :: thesis:
set YCe = ((YC . i) + 1) + (- (idseq e));
A55: ( dom (((YC . i) + 1) + (- (idseq e))) = dom (- (idseq e)) & dom (- (idseq e)) = dom (idseq e) ) by VALUED_1:def 2, VALUED_1:8;
A56: for j being Nat st j in dom (((YC . i) + 1) + (- (idseq e))) holds
(((YC . i) + 1) + (- (idseq e))) . j = ((YC . i) + 1) - j

proof

let j be Nat; :: thesis:
assume A57: j in dom (((YC . i) + 1) + (- (idseq e))) ; :: thesis:
thus (((YC . i) + 1) + (- (idseq e))) . j = ((YC . i) + 1) + ((- (idseq e)) . j) by A57, VALUED_1:def 2
.= ((YC . i) + 1) + (- ((idseq e) . j)) by VALUED_1:8
.= ((YC . i) + 1) + (- j) by A57, A55, FINSEQ_2:49
.= ((YC . i) + 1) - j ; :: thesis:

end;

rng (((YC . i) + 1) + (- (idseq e))) c= NAT

proof

let b be Integer; :: according to MEMBERED:def 11 :: thesis:
assume b in rng (((YC . i) + 1) + (- (idseq e))) ; :: thesis:
then consider a being object such that
A58: ( a in dom (((YC . i) + 1) + (- (idseq e))) & (((YC . i) + 1) + (- (idseq e))) . a = b ) by FUNCT_1:def 3;
reconsider a = a as Nat by A58;
A59: (((YC . i) + 1) + (- (idseq e))) . a = ((YC . i) + 1) - a by A56, A58;
( YC . i > e & e >= a ) by A27, A54, A55, A58, FINSEQ_1:1;
then YC . i > a by XXREAL_0:2;
then (YC . i) + 1 > a by NAT_1:13;
then ((YC . i) + 1) - a is Nat by NAT_1:21;
hence b in NAT by A58, A59, ORDINAL1:def 12; :: thesis:

end;

then reconsider YCe = ((YC . i) + 1) + (- (idseq e)) as FinSequence of NAT by FINSEQ_1:def 4;
reconsider PP = Product YCe as Element of NAT ;
A60: for b being Element of NAT st b in dom h holds
h . b divides PP

proof

let b be Element of NAT ; :: thesis:
assume A61: b in dom h ; :: thesis:
( 1 <= b & b <= x + 1 ) by A61, A9, FINSEQ_3:25;
then reconsider b1 = b - 1 as Nat ;
A62: (YY . b1) . i in { ((YY . i) . j) where i, j is Nat : S₂[i,j] } ;
then reconsider YYb1i = (YY . b1) . i as Nat by A7;
b1 + 1 <= x + 1 by A61, A9, FINSEQ_3:25;
then b1 < Segm (x + 1) by NAT_1:13;
then b1 in x + 1 by NAT_1:44;
then YC . i,YYb1i are_congruent_mod h . (b1 + 1) by A27, A54;
then A63: h . b divides (YC . i) - YYb1i by INT_1:def 4;
YYb1i in Mx by A62, XBOOLE_0:def 3;
then YYb1i <= max Mx by XXREAL_2:def 8;
then ( 0 + 1 <= YYb1i + 1 & YYb1i + 1 <= e ) by XREAL_1:7;
then A64: YYb1i + 1 in dom YCe by A55;
then A65: YCe . (YYb1i + 1) = ((YC . i) + 1) - (YYb1i + 1) by A56;
YCe . (YYb1i + 1) divides PP by A64, INT_4:32;
hence h . b divides PP by A65, A63, INT_2:9; :: thesis:

end;

Product h divides PP - 0 by A30, A60, A15, INT_4:38;
hence Product (((YC . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z1 + 1) * (K !)) by INT_1:def 4, A29; :: thesis:

end;

given Y being k -element XFinSequence of NAT , Z, e, K being Element of NAT such that A66: ( K > x & K >= (sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) ) and
A67: for i being Nat st i in k holds
Y . i > e and
A68: ( 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 !)) ) and
A69: for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ; :: thesis:
let z be Element of NAT ; :: thesis:
assume A70: z <= x ; :: thesis:
set z1 = z + 1;
set K1 = K ! ;
set ZZ = 1 + ((z + 1) * (K !));
A71: 1 + ((z + 1) * (K !)) > 1 + 0 by XREAL_1:8;
consider prim being Element of NAT such that
A72: ( prim divides 1 + ((z + 1) * (K !)) & prim <= 1 + ((z + 1) * (K !)) & prim is prime ) by A71, NAT_4:13;
deffunc H₁( object ) -> Element of omega = (Y . $1) mod prim;
consider Yz being XFinSequence such that
A73: ( len Yz = k & ( for i being Nat st i in k holds
Yz . i = H₁(i) ) ) from AFINSQ_1:sch 2();
rng Yz c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng Yz ; :: thesis:
then consider x being object such that
A74: ( x in dom Yz & Yz . x = y ) by FUNCT_1:def 3;
y = H₁(x) by A73, A74;
hence y in NAT by ORDINAL1:def 12; :: thesis:

end;

then reconsider Yz = Yz as k -element XFinSequence of NAT by A73, RELAT_1:def 19, CARD_1:def 7;
( 1 <= z + 1 & z + 1 <= x + 1 ) by A70, NAT_1:11, XREAL_1:6;
then A75: z + 1 in Seg (x + 1) ;
K >= x + 1 by A66, NAT_1:13;
then reconsider h = 1 + ((K !) * (idseq (x + 1))) as CR_Sequence by Th2;
rng h c= NAT by VALUED_0:def 6;
then A76: h is FinSequence of NAT by FINSEQ_1:def 4;
A77: ( dom h = dom ((K !) * (idseq (x + 1))) & dom ((K !) * (idseq (x + 1))) = dom (idseq (x + 1)) ) by VALUED_1:def 2, VALUED_1:def 5;
A78: h . (z + 1) = 1 + (((K !) * (idseq (x + 1))) . (z + 1)) by A75, A77, VALUED_1:def 2
.= 1 + ((K !) * ((idseq (x + 1)) . (z + 1))) by A75, A77, VALUED_1:def 5
.= 1 + ((z + 1) * (K !)) by A75, FINSEQ_2:49 ;
1 + ((z + 1) * (K !)) divides 1 + ((Z + 1) * (K !)) by A78, A68, A76, INT_4:32, A75, A77;
then A79: prim divides 1 + ((Z + 1) * (K !)) by A72, INT_2:9;
1 + ((Z + 1) * (K !)) divides (eval (p,(@ ((<%Z,x%> ^ X) ^ Y)))) - 0 by A68, INT_1:def 4;
then A80: prim divides eval (p,(@ ((<%Z,x%> ^ X) ^ Y))) by A79, INT_2:9;
reconsider E1 = eval (p,(@ ((<%Z,x%> ^ X) ^ Y))) as Integer ;
A81: K < prim

proof

assume K >= prim ; :: thesis:
then prim divides (Z + 1) * (K !) by INT_2:2, A72, NEWTON:41;
then prim divides 1 by A79, INT_2:1;
then prim = 1 by INT_2:13;
hence contradiction by A72, INT_2:def 4; :: thesis:

end;

A82: ( len <%z,x%> = 2 & 2 = len <%Z,x%> ) by CARD_1:def 7;
A83: ( len (<%z,x%> ^ X) = 2 + n & 2 + n = len (<%Z,x%> ^ X) ) by CARD_1:def 7;
A84: ( len Y = k & k = len Yz ) by CARD_1:def 7;
A85: len ((<%z,x%> ^ X) ^ Yz) = (2 + k) + n by CARD_1:def 7;
for i being Nat st i in (2 + k) + n holds
prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i)

proof

let i be Nat; :: thesis:
assume A86: i in (2 + k) + n ; :: thesis:

per cases by A86, A85, AFINSQ_1:20;

suppose A87: i in dom (<%z,x%> ^ X) ; :: thesis:

then A88: ( ((<%z,x%> ^ X) ^ Yz) . i = (<%z,x%> ^ X) . i & ((<%Z,x%> ^ X) ^ Y) . i = (<%Z,x%> ^ X) . i ) by A83, AFINSQ_1:def 3;

per cases by A87, AFINSQ_1:20;

suppose i in dom <%z,x%> ; :: thesis:

then A89: ( i in Segm 2 & (<%z,x%> ^ X) . i = <%z,x%> . i & (<%Z,x%> ^ X) . i = <%Z,x%> . i ) by A82, AFINSQ_1:def 3;

per cases by A89, NAT_1:23, NAT_1:44;

suppose i = 0 ; :: thesis:

then A90: ( ((<%Z,x%> ^ X) ^ Y) . i = Z & ((<%z,x%> ^ X) ^ Yz) . i = z ) by A87, A83, AFINSQ_1:def 3, A89;
A91: K ! ,prim are_coprime

proof

assume not K ! ,prim are_coprime ; :: thesis:
then A92: (K !) gcd prim <> 1 by INT_2:def 3;
(K !) gcd prim divides prim by INT_2:def 2;
then (K !) gcd prim = prim by A92, A72, INT_2:def 4;
then prim divides K ! by INT_2:def 2;
hence contradiction by A81, NAT_4:19, A72; :: thesis:

end;

prim divides (1 + ((Z + 1) * (K !))) - (1 + ((z + 1) * (K !))) by A79, A72, INT_5:1;
then prim divides (Z - z) * (K !) ;
hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by A90, A91, INT_2:25; :: thesis:

end;

suppose i = 1 ; :: thesis:

hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by A88, A89, INT_2:12; :: thesis:

end;

suppose ex j being Nat st
( j in dom X & i = (len <%z,x%>) + j ) ; :: thesis:

then consider j being Nat such that
A93: ( j in dom X & i = (len <%z,x%>) + j ) ;
( (<%z,x%> ^ X) . i = X . j & (<%Z,x%> ^ X) . i = X . j ) by A82, A93, AFINSQ_1:def 3;
hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by INT_2:12, A88; :: thesis:

end;

suppose ex j being Nat st
( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ; :: thesis:

then consider j being Nat such that
A94: ( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ;
A95: ( ((<%Z,x%> ^ X) ^ Y) . i = Y . j & ((<%z,x%> ^ X) ^ Yz) . i = Yz . j ) by A83, A84, A94, AFINSQ_1:def 3;
Yz . j = (Y . j) mod prim by A73, A94;
hence prim divides (((<%Z,x%> ^ X) ^ Y) . i) - (((<%z,x%> ^ X) ^ Yz) . i) by A95, A72, PEPIN:8; :: thesis:

end;

then prim divides E1 - (eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))) by A72, Th1;
then prim divides eval (p,(@ ((<%z,x%> ^ X) ^ Yz))) by INT_5:2, A80;
then |.prim.| divides |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| by INT_2:16;
then consider m being Nat such that
A96: |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| = prim * m by NAT_D:def 3;
A97: x ^2 = x * x by SQUARE_1:def 1;
for i being object st i in dom (@ ((<%z,x%> ^ X) ^ Yz)) holds
|.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= (((x ^2) + 1) * (Product (1 + X))) * e

proof

let i be object ; :: thesis:
assume i in dom (@ ((<%z,x%> ^ X) ^ Yz)) ; :: thesis:
then A98: ( i in dom ((<%z,x%> ^ X) ^ Yz) & (<%z,x%> ^ X) ^ Yz = @ ((<%z,x%> ^ X) ^ Yz) ) by HILB10_2:def 1;
reconsider i = i as Nat by A98;

per cases by A98, AFINSQ_1:20;

suppose A99: i in dom (<%z,x%> ^ X) ; :: thesis:

then A100: (@ ((<%z,x%> ^ X) ^ Yz)) . i = (<%z,x%> ^ X) . i by A98, AFINSQ_1:def 3;

per cases by A99, AFINSQ_1:20;

suppose i in dom <%z,x%> ; :: thesis:

then A101: ( i in Segm 2 & (<%z,x%> ^ X) . i = <%z,x%> . i ) by CARD_1:def 7, AFINSQ_1:def 3;
A102: (Product (1 + X)) * e >= 1 by A68, NAT_1:14;
x ^2 >= x * 1 by NAT_1:14, A97, XREAL_1:64;
then (x ^2) + 1 >= x + 0 by XREAL_1:7;
then A103: ((x ^2) + 1) * ((Product (1 + X)) * e) >= x * 1 by A102, XREAL_1:66;

per cases by A101, NAT_1:23, NAT_1:44;

suppose i = 0 ; :: thesis:

hence |.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= (((x ^2) + 1) * (Product (1 + X))) * e by A103, A70, XXREAL_0:2, A100, A101; :: thesis:

end;

suppose i = 1 ; :: thesis:

hence |.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= (((x ^2) + 1) * (Product (1 + X))) * e by A103, A100, A101; :: thesis:

end;

suppose ex j being Nat st
( j in dom X & i = (len <%z,x%>) + j ) ; :: thesis:

then consider j being Nat such that
A104: ( j in dom X & i = (len <%z,x%>) + j ) ;
A105: dom (1 + X) = dom X by VALUED_1:def 2;
then A106: (1 + X) . j <= Product (1 + X) by A104, HILB10_4:11;
(1 + X) . j = 1 + (X . j) by A104, A105, VALUED_1:def 2;
then A107: X . j <= Product (1 + X) by A106, NAT_1:13;
e * ((x ^2) + 1) >= 1 by NAT_1:14, A68;
then 1 * (X . j) <= (e * ((x ^2) + 1)) * (Product (1 + X)) by A107, XREAL_1:66;
hence |.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= (((x ^2) + 1) * (Product (1 + X))) * e by A104, AFINSQ_1:def 3, A100; :: thesis:

end;

suppose ex j being Nat st
( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ; :: thesis:

then consider j being Nat such that
A108: ( j in dom Yz & i = (len (<%z,x%> ^ X)) + j ) ;
set YE = ((Y . j) + 1) + (- (idseq e));
A109: ((<%z,x%> ^ X) ^ Yz) . i = Yz . j by A108, AFINSQ_1:def 3;
A110: Yz . j = (Y . j) mod prim by A108, A73;
A111: 1 + ((Z + 1) * (K !)) divides (Product (((Y . j) + 1) + (- (idseq e)))) - 0 by INT_1:def 4, A69, A108, A73;
A112: ( len (((Y . j) + 1) + (- (idseq e))) = len (idseq e) & len (idseq e) = e ) by CARD_1:def 7;
A113: for w being Nat st w in dom (((Y . j) + 1) + (- (idseq e))) holds
(((Y . j) + 1) + (- (idseq e))) . w = ((Y . j) + 1) - w

proof

let w be Nat; :: thesis:
assume A114: w in dom (((Y . j) + 1) + (- (idseq e))) ; :: thesis:
then w in dom (- (idseq e)) by VALUED_1:def 2;
then w in dom (idseq e) by VALUED_1:8;
then (idseq e) . w = w by FINSEQ_2:49;
then (- (idseq e)) . w = - w by VALUED_1:8;
then (((Y . j) + 1) + (- (idseq e))) . w = ((Y . j) + 1) + (- w) by A114, VALUED_1:def 2;
hence (((Y . j) + 1) + (- (idseq e))) . w = ((Y . j) + 1) - w ; :: thesis:

end;

A115: now :: thesis:

let a be Nat; :: thesis:
assume A116: a in dom (((Y . j) + 1) + (- (idseq e))) ; :: thesis:
( 1 <= a & a <= e ) by A116, A112, FINSEQ_3:25;
then reconsider a1 = a - 1 as Nat ;
a1 + 1 <= e by A116, A112, FINSEQ_3:25;
then a1 < e by NAT_1:13;
then A117: e - a1 > 0 by XREAL_1:50;
(((Y . j) + 1) + (- (idseq e))) . a = ((Y . j) + 1) - a by A116, A113;
then ((((Y . j) + 1) + (- (idseq e))) . a) + a1 > e by A67, A84, A108;
hence (((Y . j) + 1) + (- (idseq e))) . a > 0 by A117, XREAL_1:19; :: thesis:

end;

now :: thesis:

let r be object ; :: thesis:
assume r in rng (((Y . j) + 1) + (- (idseq e))) ; :: thesis:
then consider a being object such that
A118: ( a in dom (((Y . j) + 1) + (- (idseq e))) & (((Y . j) + 1) + (- (idseq e))) . a = r ) by FUNCT_1:def 3;
reconsider a = a as Nat by A118;
(((Y . j) + 1) + (- (idseq e))) . a > 0 by A115, A118;
hence r in NAT by A118, INT_1:3; :: thesis:

end;

then A119: ((Y . j) + 1) + (- (idseq e)) is FinSequence of NAT by FINSEQ_1:def 4, TARSKI:def 3;
((Y . j) + 1) + (- (idseq e)) is positive-yielding

proof

let r be Real; :: according to PARTFUN3:def 1 :: thesis:
assume r in rng (((Y . j) + 1) + (- (idseq e))) ; :: thesis:
then consider a being object such that
A120: ( a in dom (((Y . j) + 1) + (- (idseq e))) & (((Y . j) + 1) + (- (idseq e))) . a = r ) by FUNCT_1:def 3;
thus not r <= 0 by A115, A120; :: thesis:

end;

then consider w being Nat such that
A121: ( w in dom (((Y . j) + 1) + (- (idseq e))) & prim divides (((Y . j) + 1) + (- (idseq e))) . w ) by A111, A79, INT_2:9, Th12, A72, A119;
A122: ( 1 <= w & w <= e ) by A112, A121, FINSEQ_3:25;
then reconsider w1 = w - 1 as Nat ;
prim divides ((Y . j) + 1) - w by A121, A113;
then prim divides (Y . j) - w1 ;
then Yz . j = w1 mod prim by A110, INT_4:23, A72;
then Yz . j < w1 + 1 by NAT_1:13, NEWTON05:11;
then A123: Yz . j < e by A122, XXREAL_0:2;
((x ^2) + 1) * (Product (1 + X)) >= 1 by NAT_1:14;
then 1 * (Yz . j) <= e * (((x ^2) + 1) * (Product (1 + X))) by A123, XREAL_1:66;
hence |.((@ ((<%z,x%> ^ X) ^ Yz)) . i).| <= (((x ^2) + 1) * (Product (1 + X))) * e by A109, A98; :: thesis:

end;

then |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| <= (sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) by A68, NAT_1:14, Th10;
then |.(eval (p,(@ ((<%z,x%> ^ X) ^ Yz)))).| <= K by A66, XXREAL_0:2;
then prim * m < prim * 1 by A96, A81, XXREAL_0:2;
then m < 1 by XREAL_1:66;
then m = 0 by NAT_1:14;
then eval (p,(@ ((<%z,x%> ^ X) ^ Yz))) = 0 by A96;
hence ex y being k -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ; :: thesis: