hilb10_5.miz



    begin

    reserve i,j,n,n1,n2,m,k,l,u for Nat,

i1,i2,i3,i4,i5,i6 for Element of n,

p,q for n -element XFinSequence of NAT ,

a,b,c,d,e,f for Integer;

    registration

      let n be Nat;

      cluster ( idseq n) -> INT -valued;

      coherence ;

      let x be n -element natural-valued XFinSequence;

      let p be INT -valued Polynomial of n, F_Real ;

      cluster ( eval (p,( @ x))) -> integer;

      coherence

      proof

        ( @ x) is INT -valued by HILB10_2:def 1;

        hence thesis;

      end;

    end

    theorem :: HILB10_5:1

    

     Th1: for p be INT -valued Polynomial of n, F_Real holds for x,y be n -element XFinSequence of NAT st k <> 0 & for i st i in n holds k divides ((x . i) - (y . i)) holds k divides (( eval (p,( @ x))) qua Integer - ( eval (p,( @ y))) qua Integer)

    proof

      let p be INT -valued Polynomial of n, F_Real ;

      let x,y be n -element XFinSequence of NAT such that

       A1: k <> 0 and

       A2: for i st i in n holds k divides ((x . i) - (y . i));

      reconsider FR = F_Real as Field;

      reconsider pF = p as Polynomial of n, FR;

      reconsider xF = ( @ x), yF = ( @ y) as Function of n, the carrier of FR;

      set sgmF = ( SgmX (( BagOrder n),( Support pF)));

      set sgm = ( SgmX (( BagOrder n),( Support p)));

      consider X be FinSequence of the carrier of FR such that

       A3: ( len X) = ( len sgmF) & ( eval (pF,xF)) = ( Sum X) and

       A4: for i be Element of NAT st 1 <= i & i <= ( len X) holds (X /. i) = (((pF * sgmF) /. i) * ( eval ((sgmF /. i),xF))) by POLYNOM2:def 4;

      consider Y be FinSequence of the carrier of FR such that

       A5: ( len Y) = ( len sgmF) & ( eval (pF,yF)) = ( Sum Y) and

       A6: for i be Element of NAT st 1 <= i & i <= ( len Y) holds (Y /. i) = (((pF * sgmF) /. i) * ( eval ((sgmF /. i),yF))) by POLYNOM2:def 4;

      reconsider Yr = Y, Xr = X as FinSequence of REAL ;

      defpred P[ Nat] means $1 <= ( len X) implies (( Sum (Xr | $1)) - ( Sum (Yr | $1))) is Integer & for d be Integer st d = (( Sum (Xr | $1)) - ( Sum (Yr | $1))) holds k divides d;

      

       A7: P[ 0 ] by INT_2: 12;

      

       A8: for i be Nat st P[i] holds P[(i + 1)]

      proof

        

         A9: ( len (p * sgm)) = ( len sgm) by CARD_1:def 7;

        let i be Nat;

        assume

         A10: P[i];

        set i1 = (i + 1);

        set O = ((pF * sgmF) /. i1), O1 = ( eval ((sgmF /. i1),xF)), O2 = ( eval ((sgmF /. i1),yF));

        ( @ x) is INT -valued & ( @ y) is INT -valued by HILB10_2:def 1;

        then

        reconsider o1 = O1, o2 = O2 as Integer;

        assume

         A11: i1 <= ( len X);

        then

        reconsider S = (( Sum (Xr | i)) - ( Sum (Yr | i))) as Integer by A10, NAT_1: 13;

        

         A12: i1 in ( dom X) by A11, NAT_1: 11, FINSEQ_3: 25;

        then

         A13: (X | i1) = ((X | i) ^ <*(X . i1)*>) & (X . i1) = (X /. i1) & (Xr . i1) = (Xr /. i1) by FINSEQ_5: 10, PARTFUN1:def 6;

        

         A14: ( Sum (X | i)) = ( Sum (Xr | i)) by MATRPROB: 36;

        ( dom (pF * sgmF)) = ( dom X) by A3, A9, FINSEQ_3: 29;

        then ((pF * sgmF) . i1) = ((pF * sgmF) /. i1) by A12, PARTFUN1:def 6;

        then

        reconsider o = O as Integer;

        

         A15: ( Sum (Xr | i1)) = ( Sum (X | i1)) by MATRPROB: 36

        .= (( Sum (X | i)) + ( Sum <*(X /. i1)*>)) by A13, RLVECT_1: 41

        .= ( addreal . (( Sum (X | i)),(X /. i1))) by RLVECT_1: 44

        .= (( Sum (Xr | i)) + (Xr /. i1)) by A14, BINOP_2:def 9;

        i1 in ( dom Y) by A11, NAT_1: 11, FINSEQ_3: 25, A3, A5;

        then

         A16: (Y | i1) = ((Y | i) ^ <*(Y . i1)*>) & (Y . i1) = (Y /. i1) & (Yr . i1) = (Yr /. i1) by FINSEQ_5: 10, PARTFUN1:def 6;

        

         A17: ( Sum (Y | i)) = ( Sum (Yr | i)) by MATRPROB: 36;

        

         A18: ( Sum (Yr | i1)) = ( Sum (Y | i1)) by MATRPROB: 36

        .= (( Sum (Y | i)) + ( Sum <*(Y /. i1)*>)) by A16, RLVECT_1: 41

        .= ( addreal . (( Sum (Y | i)),(Y /. i1))) by RLVECT_1: 44

        .= (( Sum (Yr | i)) + (Yr /. i1)) by A17, BINOP_2:def 9;

        

         A19: (Yr /. i1) = (O * O2) by A3, A5, A6, A11, NAT_1: 11;

        reconsider OO1 = (O * O1), OO2 = (O * O2), PS = ((p * sgm) /. i1) as Element of F_Real ;

        

         A20: ((Xr /. i1) - (Yr /. i1)) = (OO1 - OO2) by A4, A11, NAT_1: 11, A19

        .= (PS * (( eval ((sgmF /. i1),( @ x))) - ( eval ((sgmF /. i1),( @ y))))) by VECTSP_1: 11

        .= (o * (o1 - o2));

        k divides (o1 - o2)

        proof

          set b = (sgmF /. i1), SG = ( SgmX (( RelIncl n),( support b)));

          consider H1 be FinSequence of FR such that

           A21: ( len H1) = ( len SG) & ( eval (b,xF)) = ( Product H1) and

           A22: for i be Element of NAT st 1 <= i & i <= ( len H1) holds (H1 /. i) = (( power FR) . (((xF * SG) /. i),((b * SG) /. i))) by POLYNOM2:def 2;

          consider H2 be FinSequence of FR such that

           A23: ( len H2) = ( len SG) & ( eval (b,yF)) = ( Product H2) and

           A24: for i be Element of NAT st 1 <= i & i <= ( len H2) holds (H2 /. i) = (( power FR) . (((yF * SG) /. i),((b * SG) /. i))) by POLYNOM2:def 2;

          defpred F[ Nat] means $1 <= ( len SG) implies ( Product (H1 | $1)) is integer & ( Product (H2 | $1)) is integer & for i1,i2 be Integer st i1 = ( Product (H1 | $1)) & i2 = ( Product (H2 | $1)) holds k divides (i1 - i2);

          reconsider ZERO = 0 as Nat;

          

           A25: F[ 0 ]

          proof

            assume 0 <= ( len SG);

            (H2 | ZERO) = ( <*> the carrier of F_Real );

            

            then ( Product (H2 | ZERO)) = ( 1_ F_Real ) by GROUP_4: 8

            .= 1;

            hence thesis by INT_2: 12;

          end;

          

           A26: for i be Nat st F[i] holds F[(i + 1)]

          proof

            let i be Nat;

            assume

             A27: F[i];

            set i1 = (i + 1), B = ((b * SG) /. i1);

            assume

             A28: i1 <= ( len SG);

            then

            reconsider p1 = ( Product (H1 | i)), p2 = ( Product (H2 | i)) as Integer by A27, NAT_1: 13;

            

             A29: i1 in ( dom SG) by NAT_1: 11, A28, FINSEQ_3: 25;

            

             A30: ( len x) = n & x = xF & y = yF by CARD_1:def 7, HILB10_2:def 1;

            ( rng SG) c= n = ( dom xF) & n = ( dom yF) by PARTFUN1:def 2, RELAT_1:def 19;

            then i1 in ( dom (xF * SG)) & i1 in ( dom (yF * SG)) by A29, RELAT_1: 27;

            then

             A31: ((xF * SG) /. i1) = ((xF * SG) . i1) & ((xF * SG) . i1) = (xF . (SG . i1)) & ((yF * SG) /. i1) = ((yF * SG) . i1) & ((yF * SG) . i1) = (yF . (SG . i1)) & (SG . i1) in ( dom xF) by PARTFUN1:def 6, FUNCT_1: 11, FUNCT_1: 12;

            then

             A32: (SG . i1) in ( dom x) by HILB10_2:def 1;

            set sg = (SG . i1);

            reconsider xS = ((xF * SG) /. i1), yS = ((yF * SG) /. i1) as Integer by A31, A30;

            reconsider xfSG = ((xF * SG) /. i1), yfSG = ((yF * SG) /. i1) as Element of F_Real ;

            (H1 /. i1) = (( power FR) . (((xF * SG) /. i1),B)) by NAT_1: 11, A22, A28, A21;

            then

             A33: (H1 /. i1) = (xS |^ B) by NIVEN: 7;

            (H2 /. i1) = (( power FR) . (((yF * SG) /. i1),B)) by NAT_1: 11, A28, A23, A24;

            then

             A34: (H2 /. i1) = (yS |^ B) by NIVEN: 7;

            i1 in ( dom H1) by A28, NAT_1: 11, FINSEQ_3: 25, A21;

            then (H1 | i1) = ((H1 | i) ^ <*(H1 . i1)*>) & (H1 . i1) = (H1 /. i1) by FINSEQ_5: 10, PARTFUN1:def 6;

            

            then

             A35: ( Product (H1 | i1)) = (( Product (H1 | i)) * (H1 /. i1)) by GROUP_4: 6

            .= (p1 * (xS |^ B)) by A33, BINOP_2:def 11;

            i1 in ( dom H2) by A28, NAT_1: 11, FINSEQ_3: 25, A23;

            then (H2 | i1) = ((H2 | i) ^ <*(H2 . i1)*>) & (H2 . i1) = (H2 /. i1) by FINSEQ_5: 10, PARTFUN1:def 6;

            

            then

             A36: ( Product (H2 | i1)) = (( Product (H2 | i)) * (H2 /. i1)) by GROUP_4: 6

            .= (p2 * (yS |^ B)) by A34, BINOP_2:def 11;

            k divides ((x . sg) - (y . sg)) by A2, A31, A32;

            then

             A37: ((xS |^ B),(yS |^ B)) are_congruent_mod k by A1, GR_CY_3: 34, INT_1:def 4, A31, A30;

            k divides (p1 - p2) by NAT_1: 13, A28, A27;

            then (p1,p2) are_congruent_mod k by INT_1:def 4;

            hence thesis by A35, A36, INT_1:def 4, A37, INT_1: 18;

          end;

          for i be Nat holds F[i] from NAT_1:sch 2( A25, A26);

          then F[( len SG)];

          hence thesis by A23, A21;

        end;

        then k divides (o * (o1 - o2)) by INT_2: 2;

        then

         A38: k divides ( - (o * (o1 - o2))) by INT_2: 10;

        k divides S by A10, A11, NAT_1: 13;

        then k divides (S - ( - (o * (o1 - o2)))) by A38, INT_5: 1;

        hence thesis by A18, A15, A20;

      end;

      

       A39: P[i] from NAT_1:sch 2( A7, A8);

      ( Sum (Xr | ( len X))) = ( eval (pF,xF)) & ( Sum (Yr | ( len X))) = ( eval (pF,yF)) by A5, A3, MATRPROB: 36;

      hence thesis by A39;

    end;

    registration

      let f be INT -valued Function;

      cluster ( - f) -> INT -valued;

      coherence ;

    end

    scheme :: HILB10_5:sch1

    SCH1 { P[ object, object], f() -> XFinSequence-yielding XFinSequence } :

{ ((f() . i) . j) where i,j be Nat : P[i, j] } is finite;

      deffunc F( object) = ( rng (f() . $1));

      consider p be XFinSequence such that

       A1: ( len p) = ( len f()) and

       A2: for k be Nat st k in ( len f()) holds (p . k) = F(k) from AFINSQ_1:sch 2;

      for X be set st X in ( rng p) holds X is finite

      proof

        let X be set such that

         A3: X in ( rng p);

        consider x be object such that

         A4: x in ( dom p) & (p . x) = X by A3, FUNCT_1:def 3;

        (p . x) = F(x) by A1, A2, A4;

        hence thesis by A4;

      end;

      then

       A5: ( union ( rng p)) is finite by FINSET_1: 7;

      { ((f() . i) . j) where i,j be Nat : P[i, j] } c= ( { 0 } \/ ( union ( rng p)))

      proof

        let x be object;

        assume x in { ((f() . i) . j) where i,j be Nat : P[i, j] };

        then

        consider i,j be Nat such that

         A6: x = ((f() . i) . j) & P[i, j];

        now

          assume not x in { 0 };

          then

           A7: x <> 0 by TARSKI:def 1;

          then j in ( dom (f() . i)) by A6, FUNCT_1:def 2;

          then

           A8: ((f() . i) . j) in ( rng (f() . i)) by FUNCT_1:def 3;

          (f() . i) <> {} by A6, A7;

          then i in ( dom f()) by FUNCT_1:def 2;

          then (f() . i) in ( rng f()) & (p . i) = F(i) & (p . i) in ( rng p) by A1, A2, FUNCT_1:def 3;

          hence x in ( union ( rng p)) by A8, A6, TARSKI:def 4;

        end;

        hence x in ( { 0 } \/ ( union ( rng p))) by XBOOLE_0:def 3;

      end;

      hence thesis by A5;

    end;

    theorem :: HILB10_5:2

    

     Th2: m >= n > 0 implies (1 + ((m ! ) * ( idseq n))) is CR_Sequence

    proof

      assume

       A1: m >= n > 0 ;

      set h = (1 + ((m ! ) * ( idseq n)));

      deffunc F( Nat) = (((m ! ) * $1) + 1);

      

       A2: ( len h) = n by CARD_1:def 7;

      

       A3: for i st i in ( dom h) holds (h . i) = F(i)

      proof

        let i such that

         A4: i in ( dom h);

        

         A5: ( dom h) = ( dom ((m ! ) * ( idseq n))) = ( dom ( idseq n)) by VALUED_1:def 2, VALUED_1:def 5;

        

        thus (h . i) = (1 + (((m ! ) * ( idseq n)) . i)) by A4, VALUED_1:def 2

        .= (1 + ((m ! ) * (( idseq n) . i))) by A4, A5, VALUED_1:def 5

        .= F(i) by A4, A5, FINSEQ_2: 49;

      end;

      

       A6: h is positive-yielding

      proof

        let r be Real;

        assume r in ( rng h);

        then

        consider x be object such that

         A7: x in ( dom h) & (h . x) = r by FUNCT_1:def 3;

        reconsider x as Nat by A7;

         F(x) > 0 ;

        hence thesis by A7, A3;

      end;

      reconsider h as non empty positive-yielding INT -valued FinSequence by A1, A6;

      

       A8: for i,j be Nat st i in ( dom h) & j in ( dom h) & i < j holds ((h . i),(h . j)) are_coprime

      proof

        let i,j be Nat such that

         A9: i in ( dom h) & j in ( dom h) & i < j;

        reconsider ji = (j - i) as Nat by A9, NAT_1: 21;

        set G = ((h . i) gcd (h . j));

        

         A10: (h . i) = F(i) & (h . j) = F(j) by A9, A3;

        then

         A11: G >= 1 by NAT_1: 14;

        assume not ((h . i),(h . j)) are_coprime ;

        then G > 1 by A11, XXREAL_0: 1, INT_2:def 3;

        then G is non trivial by NEWTON03:def 1;

        then

        consider g be prime Nat such that

         A12: g divides G by NEWTON03: 29;

        

         A13: ji <> 0 by A9;

         0 <= i & j <= n by A9, A2, FINSEQ_3: 25;

        then ji <= (n - 0 ) by XREAL_1: 13;

        then

         A14: ji divides (m ! ) by A13, NEWTON: 41, A1, XXREAL_0: 2;

        

         A15: G divides F(i) & G divides F(j) by A10, INT_2:def 2;

        then

         A16: G divides ( F(j) - F(i)) by INT_5: 1;

        

         A17: g divides F(i) by A15, A12, INT_2: 9;

        g divides ((m ! ) * ji) by A12, A16, INT_2: 9;

        then g divides (m ! ) or g divides (j - i) by INT_5: 7;

        then g divides (m ! ) by A14, INT_2: 9;

        then g divides (i * (m ! )) by INT_2: 2;

        then g divides ( F(i) - (i * (m ! ))) by A17, INT_5: 1;

        then g = 1 or g = ( - 1) by INT_2: 13;

        hence thesis by INT_2:def 4;

      end;

      h is Chinese_Remainder

      proof

        let i,j be Nat such that

         A18: i in ( dom h) & j in ( dom h) & i <> j;

        i > j or j > i by A18, XXREAL_0: 1;

        hence thesis by A18, A8;

      end;

      hence thesis;

    end;

    

     Lm1: for K,n be Nat holds ex Z be Nat st ( Product (1 + (K * ( idseq n)))) = (1 + (K * Z)) & (n > 0 implies Z > 0 )

    proof

      let K be Nat;

      defpred R[ Nat] means ex Z be Nat st ( Product (1 + (K * ( idseq $1)))) = (1 + (K * Z)) & ($1 > 0 implies Z > 0 );

      reconsider Z = 0 as Nat;

      ( Product (1 + (K * ( idseq Z)))) = (1 + (K * 0 )) by RVSUM_1: 94;

      then

       A1: R[ 0 ];

      

       A2: for n be Nat st R[n] holds R[(n + 1)]

      proof

        let n;

        assume R[n];

        then

        consider Z be Nat such that

         A3: ( Product (1 + (K * ( idseq n)))) = (1 + (K * Z)) & (n > 0 implies Z > 0 );

        set n1 = (n + 1);

        

         A4: (1 + (K * <*n1*>)) = (1 + <*(K * n1)*>) by RVSUM_1: 47

        .= <*(1 + (K * n1))*> by BASEL_1: 2;

        ( idseq n1) = (( idseq n) ^ <*(n + 1)*>) by FINSEQ_2: 51;

        then (K * ( idseq n1)) = ((K * ( idseq n)) ^ (K * <*n1*>)) by NEWTON04: 43;

        then (1 + (K * ( idseq n1))) = ((1 + (K * ( idseq n))) ^ (1 + (K * <*n1*>))) by BASEL_1: 3;

        then ( Product (1 + (K * ( idseq n1)))) = (( Product (1 + (K * ( idseq n)))) * (1 + (K * n1))) by A4, RVSUM_1: 96;

        then ( Product (1 + (K * ( idseq n1)))) = (1 + (K * ((Z + n1) + ((K * Z) * n1)))) by A3;

        hence thesis;

      end;

      for n be Nat holds R[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: HILB10_5:3

    

     Th12: for p be Prime holds for f be FinSequence of NAT st f is positive-yielding & p divides ( Product f) holds ex i st i in ( dom f) & p divides (f . i)

    proof

      let p be Prime;

      defpred P[ Nat] means for f be FinSequence of NAT st ( len f) = $1 & f is positive-yielding & p divides ( Product f) holds ex i st i in ( dom f) & p divides (f . i);

      

       A1: P[ 0 ]

      proof

        let f be FinSequence of NAT such that

         A2: ( len f) = 0 & f is positive-yielding & p divides ( Product f);

        f = ( <*> REAL ) by A2;

        hence thesis by INT_2:def 4, A2, INT_2: 27, RVSUM_1: 94;

      end;

      

       A3: P[n] implies P[(n + 1)]

      proof

        set n1 = (n + 1);

        assume

         A4: P[n];

        let f be FinSequence of NAT such that

         A5: ( len f) = n1 & f is positive-yielding & p divides ( Product f);

        f = ((f | n) ^ <*(f . n1)*>) by A5, FINSEQ_3: 55;

        then ( Product f) = (( Product (f | n)) * (f . n1)) by RVSUM_1: 96;

        per cases by NEWTON: 80, A5;

          suppose

           A6: p divides (f . n1);

          1 <= n1 by NAT_1: 11;

          hence thesis by A6, A5, FINSEQ_3: 25;

        end;

          suppose

           A7: p divides ( Product (f | n));

          ( len (f | n)) = n by A5, FINSEQ_1: 59, NAT_1: 11;

          then

          consider i such that

           A8: i in ( dom (f | n)) & p divides ((f | n) . i) by A7, A4, A5;

          i in ( dom f) & ((f | n) . i) = (f . i) by A8, FUNCT_1: 47, RELAT_1: 57;

          hence thesis by A8;

        end;

      end;

      let f be FinSequence of NAT ;

       P[n] from NAT_1:sch 2( A1, A3);

      then P[( len f)];

      hence thesis;

    end;

    begin

    definition

      let n be set, p be Series of n, F_Real ;

      :: HILB10_5:def1

      func |.p.| -> Series of n, F_Real means

      : Def1: for b be bag of n holds (it . b) = |.(p . b).|;

      existence

      proof

        defpred P[ object, object] means $2 = |.(p . $1).|;

        

         A1: for x be Element of ( Bags n) holds ex y be Element of F_Real st P[x, y]

        proof

          let x be Element of ( Bags n);

           |.(p . x).| in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider a be Function of ( Bags n), the carrier of F_Real such that

         A2: for x be Element of ( Bags n) holds P[x, (a . x)] from FUNCT_2:sch 3( A1);

        take a;

        let b be bag of n;

        b in ( Bags n) by PRE_POLY:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let a1,a2 be Series of n, F_Real such that

         A3: for b be bag of n holds (a1 . b) = |.(p . b).| and

         A4: for b be bag of n holds (a2 . b) = |.(p . b).|;

        now

          let x be Element of ( Bags n);

          

          thus (a1 . x) = |.(p . x).| by A3

          .= (a2 . x) by A4;

        end;

        hence a1 = a2;

      end;

    end

    theorem :: HILB10_5:4

    

     Th3: for n be set, p be Series of n, F_Real holds ( Support p) = ( Support |.p.|)

    proof

      let n be set, p be Series of n, F_Real ;

      

       A1: ( dom p) = ( Bags n) = ( dom |.p.|) by FUNCT_2:def 1;

      thus ( Support p) c= ( Support |.p.|)

      proof

        let x be object;

        assume x in ( Support p);

        then x in ( dom p) & (p . x) <> ( 0. F_Real ) & |.(p . x).| = ( |.p.| . x) by Def1, POLYNOM1:def 3;

        hence thesis by A1, POLYNOM1:def 3;

      end;

      let x be object;

      assume x in ( Support |.p.|);

      then x in ( dom |.p.|) & ( |.p.| . x) <> ( 0. F_Real ) & |.(p . x).| = ( |.p.| . x) by Def1, POLYNOM1:def 3;

      then x in ( dom p) & (p . x) <> ( 0. F_Real ) by A1;

      hence thesis by POLYNOM1:def 3;

    end;

    registration

      let n be Ordinal;

      let p be Polynomial of n, F_Real ;

      cluster |.p.| -> finite-Support;

      coherence

      proof

        ( Support p) = ( Support |.p.|) by Th3;

        hence thesis;

      end;

    end

    registration

      let n be set;

      let S be non empty ZeroStr;

      let p be finite-Support Series of n, S;

      cluster ( Support p) -> finite;

      coherence by POLYNOM1:def 5;

    end

    definition

      let n be Ordinal;

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be Polynomial of n, L;

      :: HILB10_5:def2

      func sum_of_coefficients p -> Element of L equals ( Sum (p * ( SgmX (( BagOrder n),( Support p)))));

      coherence ;

    end

    definition

      let n be Ordinal;

      let L be add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be Polynomial of n, L;

      :: HILB10_5:def3

      func degree p -> Nat means

      : Def3: (ex s be bag of n st s in ( Support p) & it = ( degree s)) & for s1 be bag of n st s1 in ( Support p) holds ( degree s1) <= it if p <> ( 0_ (n,L))

      otherwise it = 0 ;

      existence

      proof

        thus p <> ( 0_ (n,L)) implies ex d be Nat st (ex s be bag of n st s in ( Support p) & d = ( degree s)) & for s1 be bag of n st s1 in ( Support p) holds d >= ( degree s1)

        proof

          assume p <> ( 0_ (n,L));

          then p <> (( dom p) --> ( 0. L));

          then

          consider b be object such that

           A1: b in ( dom p) & (p . b) <> ( 0. L) by FUNCOP_1: 11;

          reconsider b as bag of n by A1;

          defpred P[ object, object] means for s be bag of n st s = $1 holds $2 = ( degree s);

          

           A2: for e be object st e in ( Support p) holds ex u be object st P[e, u]

          proof

            let e be object;

            assume e in ( Support p);

            then

            reconsider e as bag of n;

            take ( degree e);

            thus thesis;

          end;

          consider D be Function such that

           A3: ( dom D) = ( Support p) & for e be object st e in ( Support p) holds P[e, (D . e)] from CLASSES1:sch 1( A2);

          b in ( Support p) by A1, POLYNOM1:def 3;

          then ( dom D) <> {} by A3, XBOOLE_0:def 1;

          then

           A4: ( rng D) <> {} by RELAT_1: 42;

          now

            let y be object;

            assume y in ( rng D);

            then

            consider x be object such that

             A5: x in ( dom D) & y = (D . x) by FUNCT_1:def 3;

            reconsider x as bag of n by A5, A3;

            y = ( degree x) by A5, A3;

            hence y is natural;

          end;

          then

          reconsider R = ( rng D) as finite non empty natural-membered set by A4, A3, FINSET_1: 8, MEMBERED:def 6;

          ( max R) in R by XXREAL_2:def 8;

          then

          consider s be object such that

           A6: s in ( dom D) & ( max R) = (D . s) by FUNCT_1:def 3;

          reconsider s as bag of n by A6, A3;

          reconsider m = ( max R) as Nat by A6;

          take m;

          s in ( Support p) & m = ( degree s) by A6, A3;

          hence ex s be bag of n st s in ( Support p) & m = ( degree s);

          let s1 be bag of n;

          assume s1 in ( Support p);

          then (D . s1) in R & (D . s1) = ( degree s1) by FUNCT_1:def 3, A3;

          hence thesis by XXREAL_2:def 8;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let d1,d2 be Nat;

        now

          assume p <> ( 0_ (n,L));

          given s be bag of n such that

           A7: s in ( Support p) and

           A8: d1 = ( degree s);

          assume

           A9: for s1 be bag of n st s1 in ( Support p) holds d1 >= ( degree s1);

          given S be bag of n such that

           A10: S in ( Support p) and

           A11: d2 = ( degree S);

          assume

           A12: for s1 be bag of n st s1 in ( Support p) holds d2 >= ( degree s1);

          d1 <= d2 & d2 <= d1 by A7, A8, A9, A10, A11, A12;

          hence d1 = d2 by XXREAL_0: 1;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: HILB10_5:5

    

     Th4: for n be Ordinal, b be bag of n holds ( degree b) = ( Sum (b * ( SgmX (( RelIncl n),( support b)))))

    proof

      let n be Ordinal, b be bag of n;

      set SG = ( SgmX (( RelIncl n),( support b)));

      

       A1: ( RelIncl n) linearly_orders ( support b) by PRE_POLY: 82;

      

       A2: ( rng SG) = ( support b) by A1, PRE_POLY:def 2;

      then

       A3: ( rng SG) c= ( dom b) = n by PRE_POLY: 37, PARTFUN1:def 2;

      consider f be FinSequence of NAT such that

       A4: ( degree b) = ( Sum f) & f = (b * ( canFS ( support b))) by UPROOTS:def 4;

      ( rng ( canFS ( support b))) = ( support b) by FUNCT_2:def 3;

      then

      reconsider C = ( canFS ( support b)) as FinSequence of n by FINSEQ_1:def 4;

      ( rng b) c= NAT by VALUED_0:def 6;

      then

      reconsider B = b as Function of n, REAL by A3, FUNCT_2: 2;

      

       A5: SG is one-to-one by PRE_POLY: 10, PRE_POLY: 82;

      

       A6: ( rng SG) = ( rng C) by FUNCT_2:def 3, A2;

      then for x be Element of n st x in (( rng SG) \ ( rng C)) holds (B . x) = 0 by XBOOLE_0:def 1;

      hence thesis by A4, ORDERS_5: 8, A5, A6;

    end;

    theorem :: HILB10_5:6

    for n be Ordinal, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L holds ( degree p) = 0 iff ( Support p) c= {( EmptyBag n)}

    proof

      let n be Ordinal, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L;

      thus ( degree p) = 0 implies ( Support p) c= {( EmptyBag n)}

      proof

        assume

         A1: ( degree p) = 0 ;

        per cases ;

          suppose

           A2: p = ( 0_ (n,L));

          let y be object;

          assume

           A3: y in ( Support p);

          then (p . y) <> ( 0. L) by POLYNOM1:def 3;

          hence thesis by A3, A2, POLYNOM1: 22;

        end;

          suppose

           A4: p <> ( 0_ (n,L));

          let y be object;

          assume

           A5: y in ( Support p);

          then

          reconsider S = y as bag of n;

          ( degree S) = 0 by A1, A4, Def3, A5;

          then S = ( EmptyBag n) by UPROOTS: 12;

          hence y in {( EmptyBag n)} by TARSKI:def 1;

        end;

      end;

      assume

       A6: ( Support p) c= {( EmptyBag n)};

      assume

       A7: ( degree p) <> 0 ;

      then p <> ( 0_ (n,L)) by Def3;

      then

      consider s be bag of n such that

       A8: s in ( Support p) & ( degree p) = ( degree s) by Def3;

      s = ( EmptyBag n) by A6, A8, TARSKI:def 1;

      hence thesis by A7, A8, UPROOTS: 11;

    end;

    theorem :: HILB10_5:7

    

     Th6: for n be Ordinal, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, b be bag of n st b in ( Support p) holds ( degree p) >= ( degree b)

    proof

      let n be Ordinal, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, b be bag of n;

      assume

       A1: b in ( Support p);

      then ( Support p) <> {} by XBOOLE_0:def 1;

      then p <> ( 0_ (n,L)) by POLYNOM7: 1;

      hence thesis by A1, Def3;

    end;

    theorem :: HILB10_5:8

    

     Th7: for n be Ordinal, p be Polynomial of n, F_Real st |.p.| = ( 0_ (n, F_Real )) holds p = ( 0_ (n, F_Real ))

    proof

      let n be Ordinal, p be Polynomial of n, F_Real ;

      assume

       A1: |.p.| = ( 0_ (n, F_Real ));

      now

        let b be Element of ( Bags n);

         |.(p . b).| = ( |.p.| . b) by Def1

        .= 0 by A1;

        hence (p . b) = (( 0_ (n, F_Real )) . b);

      end;

      hence thesis;

    end;

    registration

      let n be set;

      reduce |.( 0_ (n, F_Real )).| to ( 0_ (n, F_Real ));

      reducibility

      proof

        now

          let b be Element of ( Bags n);

          

          thus ( |.( 0_ (n, F_Real )).| . b) = |.(( 0_ (n, F_Real )) . b).| by Def1

          .= (( 0_ (n, F_Real )) . b);

        end;

        hence thesis;

      end;

    end

    theorem :: HILB10_5:9

    for n be Ordinal, p be Polynomial of n, F_Real holds ( degree p) = ( degree |.p.|)

    proof

      let n be Ordinal, p be Polynomial of n, F_Real ;

      per cases ;

        suppose p = ( 0_ (n, F_Real ));

        hence thesis;

      end;

        suppose

         A1: p <> ( 0_ (n, F_Real ));

        then

        consider s be bag of n such that

         A2: s in ( Support p) & ( degree p) = ( degree s) by Def3;

        

         A3: |.p.| <> ( 0_ (n, F_Real )) by A1, Th7;

        then

        consider sM be bag of n such that

         A4: sM in ( Support |.p.|) & ( degree |.p.|) = ( degree sM) by Def3;

        ( Support |.p.|) = ( Support p) by Th3;

        then ( degree p) <= ( degree |.p.|) <= ( degree p) by A2, A1, Def3, A4, A3;

        hence thesis by XXREAL_0: 1;

      end;

    end;

    theorem :: HILB10_5:10

    

     Th9: for n be Ordinal, b be bag of n, r be Real st r >= 1 holds for x be Function of n, the carrier of F_Real st for i be object st i in ( dom x) holds |.(x . i).| <= r holds |.( eval (b,x)).| <= (r |^ ( degree b))

    proof

      let n be Ordinal, b be bag of n, r be Real such that

       A1: r >= 1;

      let x be Function of n, F_Real such that

       A2: for i be object st i in ( dom x) holds |.(x . i).| <= r;

      reconsider FR = F_Real as Field;

      reconsider X = x as Function of n, the carrier of F_Real ;

      set sgm = ( SgmX (( RelIncl n),( support b))), B = (b * sgm);

      

       A3: ( rng sgm) c= n = ( dom b) by PARTFUN1:def 2, RELAT_1:def 19;

      then

       A4: ( dom (b * sgm)) = ( dom sgm) by RELAT_1: 27;

      then

       A5: ( len (b * sgm)) = ( len sgm) by FINSEQ_3: 29;

      ( dom x) = n by FUNCT_2:def 1;

      then

       A6: ( dom (x * sgm)) = ( dom sgm) by A3, RELAT_1: 27;

      consider y be FinSequence of FR such that

       A7: ( len y) = ( len sgm) & ( eval (b,x)) = ( Product y) and

       A8: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (( power F_Real ) . (((x * sgm) /. i),(B /. i))) by POLYNOM2:def 2;

      ( rng B) c= NAT by VALUED_0:def 6;

      then

      reconsider B as FinSequence of NAT by FINSEQ_1:def 4;

      reconsider Y = y as FinSequence of F_Real ;

      defpred P[ Nat] means $1 <= ( len y) implies ( Product (y | $1)) is Real & for P be Real st P = ( Product (y | $1)) holds |.P.| <= (r |^ ( Sum (B | $1)));

      reconsider ZERO = 0 as Nat;

      (y | ZERO) = ( <*> the carrier of F_Real );

      then ( Product (y | ZERO)) = ( 1_ F_Real ) by GROUP_4: 8;

      then

       A9: P[ 0 ] by NEWTON: 4, RVSUM_1: 72;

      

       A10: for i st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        set i1 = (i + 1);

        assume that

         A11: P[i] and

         A12: i1 <= ( len y);

        reconsider yi1 = (y /. i1), Pi = ( Product (y | i)) as Real;

        

         A13: |.Pi.| <= (r |^ ( Sum (B | i))) by A12, A11, NAT_1: 13;

        i1 in ( dom y) by A12, NAT_1: 11, FINSEQ_3: 25;

        then (y | i1) = ((y | i) ^ <*(y . i1)*>) & (y . i1) = (y /. i1) by FINSEQ_5: 10, PARTFUN1:def 6;

        

        then

         A14: ( Product (y | i1)) = (( Product (y | i)) * (y /. i1)) by GROUP_4: 6

        .= (Pi * yi1) by BINOP_2:def 11;

        thus ( Product (y | i1)) is Real;

        let P be Real such that

         A15: P = ( Product (y | i1));

        

         A16: |.P.| = ( |.Pi.| * |.yi1.|) by A15, A14, COMPLEX1: 65;

        i1 in ( dom B) by A7, A12, A4, NAT_1: 11, FINSEQ_3: 25;

        then

         A17: (B | i1) = ((B | i) ^ <*(B . i1)*>) & (B . i1) = (B /. i1) & (B . i1) = (b . (sgm . i1)) by FINSEQ_5: 10, PARTFUN1:def 6, FUNCT_1: 12;

        then ( Sum (B | i1)) = (( Sum (B | i)) + (B /. i1)) by RVSUM_1: 74;

        then

         A18: (r |^ ( Sum (B | i1))) = ((r |^ ( Sum (B | i))) * (r |^ (B /. i1))) by NEWTON: 8;

        

         A19: |.yi1.| <= (r |^ (B /. i1))

        proof

          (y /. i1) = (( power F_Real ) . (((x * sgm) /. i1),(B /. i1))) by A8, A12, NAT_1: 11

          .= (((x * sgm) /. i1) |^ (B /. i1)) by NIVEN: 7;

          then

           A20: |.yi1.| = ( |.((x * sgm) /. i1).| |^ (B /. i1)) by TAYLOR_2: 1;

          i1 in ( dom (x * sgm)) by A6, A7, A12, NAT_1: 11, FINSEQ_3: 25;

          then

           A21: ((x * sgm) /. i1) = ((x * sgm) . i1) & ((x * sgm) . i1) = (x . (sgm . i1)) & (sgm . i1) in ( dom x) & i1 in ( dom sgm) by PARTFUN1:def 6, FUNCT_1: 11, FUNCT_1: 12;

          ( RelIncl n) linearly_orders ( support b) by PRE_POLY: 82;

          then (sgm . i1) in ( rng sgm) = ( support b) by A21, FUNCT_1:def 3, PRE_POLY:def 2;

          then (B /. i1) <> 0 by A17, PRE_POLY:def 7;

          then

           A22: (B /. i1) >= (1 + 0 ) by NAT_1: 13;

          per cases by COMPLEX1: 46;

            suppose |.((x * sgm) /. i1).| > 0 ;

            hence thesis by A20, A2, A21, PREPOWER: 9;

          end;

            suppose |.((x * sgm) /. i1).| = 0 ;

            then ( |.((x * sgm) /. i1).| |^ (B /. i1)) = 0 by A22, NEWTON: 11;

            hence thesis by A1, A20;

          end;

        end;

        

         A23: |.Pi.| >= 0 by COMPLEX1: 46;

         |.yi1.| >= 0 by COMPLEX1: 46;

        hence thesis by A13, A18, A23, A16, A19, XREAL_1: 66;

      end;

      for i holds P[i] from NAT_1:sch 2( A9, A10);

      then P[( len y)];

      then |.( eval (b,x)).| <= (r |^ ( Sum (B | ( len B)))) by A5, A7;

      hence thesis by Th4;

    end;

    theorem :: HILB10_5:11

    

     Th10: for n be Ordinal, p be Polynomial of n, F_Real , r be Real st r >= 1 holds for x be Function of n, the carrier of F_Real st for i be object st i in ( dom x) holds |.(x . i).| <= r holds |.( eval (p,x)).| <= (( sum_of_coefficients |.p.|) * (r |^ ( degree p)))

    proof

      let n be Ordinal, p be Polynomial of n, F_Real , r be Real such that

       A1: r >= 1;

      let x be Function of n, the carrier of F_Real such that

       A2: for i be object st i in ( dom x) holds |.(x . i).| <= r;

      reconsider FR = F_Real as Field;

      reconsider pF = p, ApF = |.p.| as Polynomial of n, FR;

      reconsider xF = x as Function of n, the carrier of FR;

      set sgm = ( SgmX (( BagOrder n),( Support p)));

      set SgmF = ( SgmX (( BagOrder n),( Support pF)));

      reconsider H = (ApF * SgmF) as FinSequence of the carrier of F_Real ;

      

       A3: ( sum_of_coefficients |.p.|) = ( Sum (ApF * SgmF)) by Th3;

      consider y be FinSequence of the carrier of FR such that

       A4: ( len y) = ( len SgmF) & ( eval (p,x)) = ( Sum y) and

       A5: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((pF * SgmF) /. i) * ( eval ((SgmF /. i),xF))) by POLYNOM2:def 4;

      reconsider Y = y as FinSequence of REAL ;

      defpred P[ Nat] means $1 <= ( len y) implies |.( Sum (Y | $1)).| <= (( Sum (H | $1)) * (r |^ ( degree p)));

      

       A6: P[ 0 ];

      

       A7: ( len (ApF * SgmF)) = ( len SgmF) by CARD_1:def 7;

      

       A8: for i be Nat st P[i] holds P[(i + 1)]

      proof

        

         A9: ( BagOrder n) linearly_orders ( Support p) by POLYNOM2: 18;

        

         A10: ( rng sgm) = ( Support p) by A9, PRE_POLY:def 2;

        

         A11: ( len (p * sgm)) = ( len sgm) by CARD_1:def 7;

        let i be Nat;

        assume

         A12: P[i];

        set i1 = (i + 1);

        assume

         A13: i1 <= ( len y);

        then i1 in ( dom y) by NAT_1: 11, FINSEQ_3: 25;

        then

         A14: (y | i1) = ((y | i) ^ <*(y . i1)*>) & (y . i1) = (y /. i1) & (Y . i1) = (Y /. i1) by FINSEQ_5: 10, PARTFUN1:def 6;

        

         A15: ( Sum (y | i)) = ( Sum (Y | i)) by MATRPROB: 36;

        

         A16: ( Sum (Y | i1)) = ( Sum (y | i1)) by MATRPROB: 36

        .= (( Sum (y | i)) + ( Sum <*(y /. i1)*>)) by A14, RLVECT_1: 41

        .= ( addreal . (( Sum (y | i)),(y /. i1))) by RLVECT_1: 44

        .= (( Sum (Y | i)) + (Y /. i1)) by A15, BINOP_2:def 9;

        i1 in ( dom (ApF * SgmF)) by A4, A13, A7, NAT_1: 11, FINSEQ_3: 25;

        then

         A17: (H | i1) = ((H | i) ^ <*(H . i1)*>) & (H /. i1) = (H . i1) & ((ApF * SgmF) /. i1) = ((ApF * SgmF) . i1) & ((ApF * SgmF) . i1) = (ApF . (SgmF . i1)) by FINSEQ_5: 10, PARTFUN1:def 6, FUNCT_1: 12;

        

         A18: ( Sum (H | i1)) = ( Sum ((ApF * SgmF) | i1)) by MATRPROB: 36

        .= (( Sum ((ApF * SgmF) | i)) + ( Sum <*((ApF * SgmF) /. i1)*>)) by A17, RLVECT_1: 41

        .= (the addF of FR . (( Sum ((ApF * SgmF) | i)),((ApF * SgmF) /. i1))) by RLVECT_1: 44

        .= ( addreal . (( Sum (H | i)),(H /. i1))) by MATRPROB: 36

        .= (( Sum (H | i)) + (H /. i1)) by BINOP_2:def 9;

        

         A19: |.((p * sgm) /. i1).| >= 0 & |.( eval ((sgm /. i1),x)).| >= 0 by COMPLEX1: 46;

        

         A20: (((pF * SgmF) /. i1) * ( eval ((SgmF /. i1),xF))) = (((p * sgm) /. i1) * ( eval ((sgm /. i1),x))) by BINOP_2:def 11;

        i1 in ( dom (p * sgm)) by A4, A13, A11, NAT_1: 11, FINSEQ_3: 25;

        then

         A21: ((p * sgm) . i1) = ((p * sgm) /. i1) & ((p * sgm) . i1) = (p . (sgm . i1)) & i1 in ( dom sgm) by PARTFUN1:def 6, FUNCT_1: 11, FUNCT_1: 12;

        then

         A22: (sgm . i1) in ( rng sgm) & (sgm . i1) = (sgm /. i1) by FUNCT_1:def 3, PARTFUN1:def 6;

        

         A23: (H /. i1) = ( |.p.| . (sgm /. i1)) by A17, A21, PARTFUN1:def 6

        .= |.(p . (sgm /. i1)).| by Def1;

        

         A24: |.((p * sgm) /. i1).| <= (H /. i1) by PARTFUN1:def 6, A21, A23;

        

         A25: (r |^ ( degree (sgm /. i1))) <= (r |^ ( degree p)) by A1, PREPOWER: 93, Th6, A22, A10;

         |.( eval ((sgm /. i1),x)).| <= (r |^ ( degree (sgm /. i1))) by A1, A2, Th9;

        then |.( eval ((sgm /. i1),x)).| <= (r |^ ( degree p)) by A25, XXREAL_0: 2;

        then ( |.((p * sgm) /. i1).| * |.( eval ((sgm /. i1),x)).|) <= ((H /. i1) * (r |^ ( degree p))) by A24, A19, XREAL_1: 66;

        then

         A26: |.(((p * sgm) /. i1) * ( eval ((sgm /. i1),x))).| <= ((H /. i1) * (r |^ ( degree p))) by COMPLEX1: 65;

        

         A27: |.(Y /. i1).| <= ((H /. i1) * (r |^ ( degree p))) by A20, A26, A5, A13, NAT_1: 11;

        

         A28: ( |.( Sum (Y | i)).| + |.(Y /. i1).|) >= |.(( Sum (Y | i)) + (Y /. i1)).| by COMPLEX1: 56;

        ( |.( Sum (Y | i)).| + |.(Y /. i1).|) <= ((( Sum (H | i)) * (r |^ ( degree p))) + ((H /. i1) * (r |^ ( degree p)))) by A27, XREAL_1: 7, A13, A12, NAT_1: 13;

        hence thesis by A16, A18, A28, XXREAL_0: 2;

      end;

      

       A29: ( eval (p,x)) = ( Sum (Y | ( len y))) by A4, MATRPROB: 36;

      

       A30: ( Sum (H | ( len H))) = ( sum_of_coefficients |.p.|) by A3, MATRPROB: 36;

      for i be Nat holds P[i] from NAT_1:sch 2( A6, A8);

      hence thesis by A30, A7, A4, A29;

    end;

    registration

      let n be Ordinal, p be INT -valued Polynomial of n, F_Real ;

      cluster |.p.| -> natural-valued;

      coherence

      proof

        now

          let y be object;

          assume y in ( rng |.p.|);

          then

          consider x be object such that

           A1: x in ( dom |.p.|) & ( |.p.| . x) = y by FUNCT_1:def 3;

          ( |.p.| . x) = |.(p . x).| by A1, Def1;

          hence y in NAT by A1, ORDINAL1:def 12;

        end;

        hence thesis by VALUED_0:def 6, TARSKI:def 3;

      end;

    end

    registration

      let n be Ordinal;

      cluster natural-valued for Polynomial of n, F_Real ;

      existence

      proof

        take |. the INT -valued Polynomial of n, F_Real .|;

        thus thesis;

      end;

    end

    registration

      let O be Ordinal, p be natural-valued Polynomial of O, F_Real ;

      cluster ( sum_of_coefficients p) -> natural;

      coherence

      proof

        reconsider FR = F_Real as Field;

        reconsider P = p as Polynomial of O, FR;

        set S = ( SgmX (( BagOrder O),( Support P)));

        consider f be sequence of FR such that

         A1: ( Sum (P * S)) = (f . ( len (P * S))) & (f . 0 ) = ( 0. FR) and

         A2: for j be Nat holds for v be Element of FR st j < ( len (P * S)) & v = ((P * S) . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

        defpred P[ Nat] means $1 <= ( len (P * S)) implies (f . $1) is natural;

        

         A3: P[ 0 ] by A1;

        

         A4: P[n] implies P[(n + 1)]

        proof

          set n1 = (n + 1);

          assume

           A5: P[n];

          assume

           A6: n1 <= ( len (P * S));

          then

           A7: n1 in ( dom (P * S)) by NAT_1: 11, FINSEQ_3: 25;

          

           A8: ((P * S) . n1) = ((P * S) /. n1) by A7, PARTFUN1:def 6;

          reconsider psn1 = ((P * S) /. n1) as Nat by A8;

          reconsider fn = (f . n) as Nat by A5, A6, NAT_1: 13;

          ((f . n) + ((P * S) /. n1)) = (fn + psn1) by BINOP_2:def 9;

          hence thesis by A8, A2, A6, NAT_1: 13;

        end;

         P[n] from NAT_1:sch 2( A3, A4);

        hence thesis by A1;

      end;

    end

    begin

    scheme :: HILB10_5:sch2

    SubsetDioph { n() -> Nat , P[ Nat, Nat, Nat, Nat], S() -> set } :

for i2,i3,i4 be Element of n() holds { p where p be n() -element XFinSequence of NAT : for i be Nat st i in S() holds P[(p . i), (p . i2), (p . i3), (p . i4)] } is diophantine Subset of (n() -xtuples_of NAT )

      provided

       A1: for i1,i2,i3,i4 be Element of n() holds { p where p be n() -element XFinSequence of NAT : P[(p . i1), (p . i2), (p . i3), (p . i4)] } is diophantine Subset of (n() -xtuples_of NAT )

       and

       A2: S() c= ( Segm n());

      reconsider S = S() as finite set by A2;

      defpred R[ Nat] means for X be finite set st X c= S & ( card X) = $1 holds for i2,i3,i4 be Element of n() holds { p where p be n() -element XFinSequence of NAT : for i st i in X holds P[(p . i), (p . i2), (p . i3), (p . i4)] } is diophantine Subset of (n() -xtuples_of NAT );

      

       A3: R[ 0 ]

      proof

        let X be finite set such that

         A4: X c= S & ( card X) = 0 ;

        let i2,i3,i4 be Element of n();

        set PP = { p where p be n() -element XFinSequence of NAT : for i be Nat st i in X holds P[(p . i), (p . i2), (p . i3), (p . i4)] };

        

         A5: PP c= ( [#] (n() -xtuples_of NAT ))

        proof

          let x be object;

          assume x in PP;

          then ex p be n() -element XFinSequence of NAT st x = p & for i be Nat st i in X holds P[(p . i), (p . i2), (p . i3), (p . i4)];

          hence thesis by HILB10_2:def 5;

        end;

        ( [#] (n() -xtuples_of NAT )) c= PP

        proof

          let x be object;

          assume x in ( [#] (n() -xtuples_of NAT ));

          then

          reconsider p = x as n() -element XFinSequence of NAT ;

          X = {} by A4;

          then for i be Nat st i in X holds P[(p . i), (p . i2), (p . i3), (p . i4)] by XBOOLE_0:def 1;

          hence thesis;

        end;

        hence thesis by A5, XBOOLE_0:def 10;

      end;

      

       A6: for m st R[m] holds R[(m + 1)]

      proof

        let m such that

         A7: R[m];

        let X be finite set such that

         A8: X c= S & ( card X) = (m + 1);

        let i2,i3,i4 be Element of n();

        X is non empty by A8;

        then

        consider x be object such that

         A9: x in X by XBOOLE_0:def 1;

        x in S by A8, A9;

        then

        reconsider x as Element of n() by A2;

        defpred Pn1[ XFinSequence of NAT ] means for i be Nat st i in (X \ {x}) holds P[($1 . i), ($1 . i2), ($1 . i3), ($1 . i4)];

        ( card (X \ {x})) = m by A8, A9, STIRL2_1: 55;

        then

         A10: { p where p be n() -element XFinSequence of NAT : Pn1[p] } is diophantine Subset of (n() -xtuples_of NAT ) by A8, XBOOLE_1: 1, A7;

        defpred P1[ XFinSequence of NAT ] means P[($1 . x), ($1 . i2), ($1 . i3), ($1 . i4)];

        

         A11: { p where p be n() -element XFinSequence of NAT : P1[p] } is diophantine Subset of (n() -xtuples_of NAT ) by A1;

        defpred P[ XFinSequence of NAT ] means Pn1[$1] & P1[$1];

        

         A12: { p where p be n() -element XFinSequence of NAT : Pn1[p] & P1[p] } is diophantine Subset of (n() -xtuples_of NAT ) from HILB10_3:sch 3( A10, A11);

        defpred Q[ XFinSequence of NAT ] means for i be Nat st i in X holds P[($1 . i), ($1 . i2), ($1 . i3), ($1 . i4)];

        

         A13: for p be n() -element XFinSequence of NAT holds P[p] iff Q[p]

        proof

          let p be n() -element XFinSequence of NAT ;

          thus P[p] implies Q[p]

          proof

            assume

             A14: P[p];

            let i be Nat such that

             A15: i in X;

            i = x or not i in {x} by TARSKI:def 1;

            then i = x or i in (X \ {x}) by A15, XBOOLE_0:def 5;

            hence thesis by A14;

          end;

          assume Q[p];

          hence thesis by A9, A2;

        end;

        { p where p be n() -element XFinSequence of NAT : P[p] } = { p where p be n() -element XFinSequence of NAT : Q[p] } from HILB10_3:sch 2( A13);

        hence thesis by A12;

      end;

      for m holds R[m] from NAT_1:sch 2( A3, A6);

      then R[( card S)];

      hence thesis;

    end;

    theorem :: HILB10_5:12

    

     Th11: for k, n1, n2, i, j, l, m, n, i1, i2, i3, i4 st (n1 + n2) <= n holds { p : (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 )

    proof

      let k, n1, n2, i, j, l, m;

      deffunc F0( Nat, Nat, Nat) = ($1 |^ $2);

      

       A1: for n, i1, i2, i3, i4 holds { p : F0(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 24;

      defpred P0[ Nat, Nat, natural object, Nat, Nat, Nat] means (1 * $1) >= ((k * $3) + 0 );

      

       A2: for n, i1, i2, i3, i4, i5, i6 holds { p : P0[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 8;

      

       A3: for i1, i2, i3, i4, i5 holds { p : P0[(p . i1), (p . i2), F0(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A2, A1);

      deffunc F1( Nat, Nat, Nat) = ((i * $1) + j);

      

       A4: for n, i1, i2, i3, i4 holds { p : F1(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 15;

      defpred P1[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 >= (k * ($2 |^ $3));

       A5:

      now

        let n, i1, i2, i3, i4, i5, i6;

        defpred Q1[ XFinSequence of NAT ] means P0[($1 . i1), ($1 . i2), (($1 . i2) |^ ($1 . i3)), ($1 . i4), ($1 . i5), ($1 . i6)];

        defpred Q2[ XFinSequence of NAT ] means P1[($1 . i1), ($1 . i2), ($1 . i3), ($1 . i4), ($1 . i5), ($1 . i6)];

        

         A6: for p holds Q1[p] iff Q2[p];

        { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A6);

        hence { p : P1[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by A3;

      end;

      

       A7: for i1, i2, i3, i4, i5 holds { p : P1[(p . i1), (p . i2), F1(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A5, A4);

      deffunc F2( Nat, Nat, Nat) = ((1 * $1) * $2);

      

       A8: for n, i1, i2, i3, i4 holds { p : F2(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_4: 26;

      defpred P2[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 >= (k * ($3 |^ ((i * $2) + j)));

      

       A9: for n, i1, i3, i2, i4, i5, i6 holds { p : P2[(p . i1), (p . i3), (p . i2), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by A7;

      

       A10: for i1, i2, i3, i4, i5 holds { p : P2[(p . i1), (p . i2), F2(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A9, A8);

      defpred P3[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 >= (k * (($6 * $3) |^ ((i * $2) + j)));

       A11:

      now

        let n, i1, i2, i4, i5, i6, i3;

        defpred Q1[ XFinSequence of NAT ] means P2[($1 . i1), ($1 . i2), ((1 * ($1 . i3)) * ($1 . i4)), ($1 . i4), ($1 . i5), ($1 . i5)];

        defpred Q2[ XFinSequence of NAT ] means P3[($1 . i1), ($1 . i2), ($1 . i4), ($1 . i5), ($1 . i6), ($1 . i3)];

        

         A12: for p holds Q1[p] iff Q2[p];

        { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A12);

        hence { p : P3[(p . i1), (p . i2), (p . i4), (p . i5), (p . i6), (p . i3)] } is diophantine Subset of (n -xtuples_of NAT ) by A10;

      end;

      

       A13: for i1, i2, i3, i4, i5 holds { p : P3[(p . i1), (p . i2), F2(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A11, A8);

      deffunc F5( Nat, Nat, Nat) = ((1 * $1) + 1);

      

       A14: for n, i1, i2, i3, i4 holds { p : F5(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 15;

      defpred P5[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 >= (k * ((($3 * $5) * $6) |^ ((i * $2) + j)));

       A15:

      now

        let n, i1, i2, i4, i3, i5, i6;

        defpred Q1[ XFinSequence of NAT ] means P3[($1 . i1), ($1 . i2), ((1 * ($1 . i4)) * ($1 . i5)), ($1 . i4), ($1 . i5), ($1 . i6)];

        defpred Q2[ XFinSequence of NAT ] means P5[($1 . i1), ($1 . i2), ($1 . i4), ($1 . i3), ($1 . i5), ($1 . i6)];

        

         A16: for p holds Q1[p] iff Q2[p];

        { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A16);

        hence { p : P5[(p . i1), (p . i2), (p . i4), (p . i3), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by A13;

      end;

      

       A17: for i1, i2, i3, i4, i5 holds { p : P5[(p . i1), (p . i2), F5(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A15, A14);

      deffunc G1( Nat, Nat, Nat) = ((l * $1) + m);

      

       A18: for n, i1, i2, i3, i4 holds { p : G1(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 15;

      defpred R1[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 >= (k * ((($3 * $5) * ($6 + 1)) |^ ((i * $2) + j)));

       A19:

      now

        let n, i1, i2, i6, i4, i5, i3;

        defpred Q1[ XFinSequence of NAT ] means P5[($1 . i1), ($1 . i2), ((1 * ($1 . i3)) + 1), ($1 . i4), ($1 . i5), ($1 . i6)];

        defpred Q2[ XFinSequence of NAT ] means R1[($1 . i1), ($1 . i2), ($1 . i6), ($1 . i4), ($1 . i5), ($1 . i3)];

        

         A20: for p holds Q1[p] iff Q2[p];

        { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A20);

        hence { p : R1[(p . i1), (p . i2), (p . i6), (p . i4), (p . i5), (p . i3)] } is diophantine Subset of (n -xtuples_of NAT ) by A17;

      end;

      

       A21: for i1, i2, i3, i4, i5 holds { p : R1[(p . i1), (p . i2), G1(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A19, A18);

      defpred P6[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 >= (k * (((($3 + 1) * $5) * ((l * $6) + m)) |^ ((i * $2) + j)));

      deffunc F6( Nat, Nat, Nat) = ((1 * $1) * $1);

      

       A22: for n, i1, i2, i3, i4 holds { p : F6(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_4: 26;

       A23:

      now

        let n, i1, i2, i6, i4, i5, i3;

        defpred Q1[ XFinSequence of NAT ] means R1[($1 . i1), ($1 . i2), ((l * ($1 . i3)) + m), ($1 . i4), ($1 . i5), ($1 . i6)];

        defpred Q2[ XFinSequence of NAT ] means P6[($1 . i1), ($1 . i2), ($1 . i6), ($1 . i4), ($1 . i5), ($1 . i3)];

        

         A24: for p holds Q1[p] iff Q2[p];

        { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A24);

        hence { p : P6[(p . i1), (p . i2), (p . i6), (p . i4), (p . i5), (p . i3)] } is diophantine Subset of (n -xtuples_of NAT ) by A21;

      end;

      

       A25: for n, i1, i2, i3, i4, i5 holds { p : P6[(p . i1), (p . i2), F6(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A23, A22);

      let n, i1, i2, i3, i4 such that

       A26: (n1 + n2) <= n;

      set X = (n + 1);

      

       A27: n < X by NAT_1: 13;

      then n in ( Segm X) by NAT_1: 44;

      then

      reconsider N = n, I1 = i1, I2 = i2, I3 = i3, I4 = i4 as Element of X by HILB10_3: 2;

      defpred P7[ XFinSequence of NAT ] means ($1 . I1) >= (k * ((((((1 * ($1 . I2)) * ($1 . I2)) + 1) * ($1 . N)) * ((l * ($1 . I3)) + m)) |^ ((i * ($1 . I4)) + j)));

      

       A28: { p where p be X -element XFinSequence of NAT : P7[p] } is diophantine Subset of (X -xtuples_of NAT ) by A25;

      defpred Q7[ XFinSequence of NAT ] means ($1 . N) = ( Product (1 + (($1 /^ n1) | n2)));

      

       A29: { p where p be X -element XFinSequence of NAT : Q7[p] } is diophantine Subset of (X -xtuples_of NAT ) by HILB10_4: 39;

      set PQ = { p where p be X -element XFinSequence of NAT : P7[p] & Q7[p] };

      

       A30: PQ is diophantine Subset of (X -xtuples_of NAT ) from HILB10_3:sch 3( A28, A29);

      set PQr = { (p | n) where p be X -element XFinSequence of NAT : p in PQ };

      defpred S[ XFinSequence of NAT ] means ($1 . i1) >= (k * (((((($1 . i2) ^2 ) + 1) * ( Product (1 + (($1 /^ n1) | n2)))) * ((l * ($1 . i3)) + m)) |^ ((i * ($1 . i4)) + j)));

      set S = { p : S[p] };

      

       A31: PQr is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 5, A27, A30;

      

       A32: n1 <= (n1 + n2) by NAT_1: 11;

      

       A33: (n -' n1) = (n - n1) by A32, A26, XXREAL_0: 2, XREAL_1: 233;

      

       A34: n2 <= (n - n1) by A26, XREAL_1: 19;

      S c= (n -xtuples_of NAT )

      proof

        let y be object;

        assume y in S;

        then ex p st y = p & S[p];

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider S as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then S is diophantine Subset of (n -xtuples_of NAT );

        hence thesis;

      end;

        suppose

         A35: n <> 0 ;

        

         A36: S c= PQr

        proof

          let y be object;

          assume y in S;

          then

          consider p such that

           A37: y = p & S[p];

          

           A38: ( len p) = n by CARD_1:def 7;

          then

           A39: ( len (p /^ n1)) >= n2 by A34, A33, AFINSQ_2:def 2;

          reconsider P = ( Product (1 + ((p /^ n1) | n2))) as Element of NAT by ORDINAL1:def 12;

          reconsider pP = (p ^ <%P%>) as X -element XFinSequence of NAT ;

          

           A40: (pP | n) = p by A38, AFINSQ_1: 57;

          

           A41: (pP . N) = P by A38, AFINSQ_1: 36;

          

           A42: (pP . I1) = (p . i1) & (pP . I2) = (p . i2) & (pP . I3) = (p . i3) & (pP . I4) = (p . i4) by A35, A40, HILB10_3: 4;

          

           A43: ((pP /^ n1) | n2) = (((p /^ n1) ^ <%P%>) | n2) by HILB10_4: 10, A38, A32, A26, XXREAL_0: 2

          .= ((p /^ n1) | n2) by AFINSQ_1: 58, A39;

           P7[pP] & Q7[pP] by A43, A42, A41, A37, SQUARE_1:def 1;

          then pP in PQ;

          hence thesis by A37, A40;

        end;

        PQr c= S

        proof

          let y be object;

          assume y in PQr;

          then

          consider pP be X -element XFinSequence of NAT such that

           A44: y = (pP | n) & pP in PQ;

          

           A45: ex q be X -element XFinSequence of NAT st pP = q & P7[q] & Q7[q] by A44;

          

           A46: ( len pP) = X by CARD_1:def 7;

          then

           A47: ( len (pP | n)) = n by A27, AFINSQ_1: 54;

          then

          reconsider p = (pP | n) as n -element XFinSequence of NAT by CARD_1:def 7;

          

           A48: ( len (p /^ n1)) >= n2 by A34, A33, A47, AFINSQ_2:def 2;

          set P = ( Product (1 + ((p /^ n1) | n2)));

          

           A49: pP = (p ^ <%(pP . n)%>) by A46, AFINSQ_1: 56;

          

           A50: ((pP /^ n1) | n2) = (((p /^ n1) ^ <%(pP . n)%>) | n2) by A49, HILB10_4: 10, A47, A32, A26, XXREAL_0: 2

          .= ((p /^ n1) | n2) by AFINSQ_1: 58, A48;

          

           A51: (pP . I1) = (p . i1) & (pP . I2) = (p . i2) & (pP . I3) = (p . i3) & (pP . I4) = (p . i4) by A35, HILB10_3: 4;

          ((p . i2) * (p . i2)) = ((p . i2) ^2 ) by SQUARE_1:def 1;

          hence thesis by A44, A50, A51, A45;

        end;

        hence thesis by A31, A36, XBOOLE_0:def 10;

      end;

    end;

    theorem :: HILB10_5:13

    

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

    proof

      let P be INT -valued Polynomial of k, F_Real , a be Integer, perm be Permutation of n, i1 such that

       A1: k <= n;

      defpred P[ XFinSequence of NAT ] means for q be k -element XFinSequence of NAT st q = (($1 * perm) | k) holds (a * ($1 . i1)) = ( eval (P,( @ q)));

      set A = { p : P[p] };

      A c= (n -xtuples_of NAT )

      proof

        let y be object such that

         A2: y in A;

        ex p be n -element XFinSequence of NAT st y = p & P[p] by A2;

        hence thesis by HILB10_2:def 5;

      end;

      then

      reconsider A as Subset of (n -xtuples_of NAT );

      per cases ;

        suppose n = 0 ;

        then A is diophantine;

        hence thesis;

      end;

        suppose

         A3: n <> 0 ;

        reconsider nk = (n - k) as Nat by A1, NAT_1: 21;

        consider Q be Polynomial of (k + nk), F_Real such that

         A4: ( rng Q) c= (( rng P) \/ {( 0. F_Real )}) and

         A5: for x be Function of k, F_Real , y be Function of (k + nk), F_Real st (y | k) = x holds ( eval (P,x)) = ( eval (Q,y)) by HILB10_2: 27;

        

         A6: ( rng P) c= INT by RELAT_1:def 19;

        ( 0. F_Real ) in INT by INT_1:def 1;

        then {( 0. F_Real )} c= INT by ZFMISC_1: 31;

        then (( rng P) \/ {( 0. F_Real )}) c= INT by A6, XBOOLE_1: 8;

        then

        reconsider Q1 = Q as INT -valued Polynomial of n, F_Real by RELAT_1:def 19, A4, XBOOLE_1: 1;

        set T = (Q1 permuted_by perm);

        

         A7: ( rng T) = ( rng Q1) by HILB10_2: 26;

        ( rng Q1) c= INT by RELAT_1:def 19;

        then

        reconsider T1 = T as INT -valued Polynomial of n, F_Real by A7, RELAT_1:def 19;

        reconsider FR = F_Real as Field;

        reconsider ar = a as Element of FR by XREAL_0:def 1;

        reconsider Ar = ar as Element of F_Real ;

        reconsider t = T as Polynomial of n, FR;

        T1 = t;

        then

        reconsider TI = (t - (ar * ( 1_1 (i1,FR)))) as INT -valued Polynomial of (n + 0 ), F_Real ;

        for s be object holds s in A iff ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (TI,( @ (x ^ y)))) = 0

        proof

          let s be object;

          thus s in A implies ex x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT st s = x & ( eval (TI,( @ (x ^ y)))) = 0

          proof

            assume s in A;

            then

            consider p be n -element XFinSequence of NAT such that

             A8: s = p & P[p];

            reconsider E = ( <%> NAT ) as 0 -element XFinSequence of NAT ;

            take p, E;

            thus s = p by A8;

            reconsider pE = ( @ (p ^ E)) as Function of n, FR;

            

             A9: ( eval (( 1_1 (i1,FR)),pE)) = (pE . i1) by A3, HILB10_3: 1

            .= (p . i1) by HILB10_2:def 1;

            reconsider Eval = ( eval (( 1_1 (i1,FR)),pE)) as Element of F_Real ;

            

             A10: ( eval ((ar * ( 1_1 (i1,FR))),pE)) = (Ar * Eval) by POLYNOM7: 29

            .= (a * (p . i1)) by A9;

            

             A11: ( dom perm) = n & ( rng perm) = n & ( len p) = n by FUNCT_2: 52, FUNCT_2:def 3, CARD_1:def 7;

            then ( dom (p * perm)) = n by RELAT_1: 27;

            then

            reconsider pp = (p * perm) as XFinSequence by AFINSQ_1: 5;

            

             A12: ( len pp) = n by A11, RELAT_1: 27;

            reconsider PP = pp as n -element XFinSequence of NAT by A12, CARD_1:def 7;

            ( len (PP | k)) = k by A12, A1, AFINSQ_1: 54;

            then

            reconsider PPk = (PP | k) as k -element XFinSequence of NAT by CARD_1:def 7;

            (( @ PP) | k) = (PP | k) by HILB10_2:def 1;

            then

             A13: (( @ PP) | k) = ( @ PPk) by HILB10_2:def 1;

            (PP * (perm " )) = (p * (perm * (perm " ))) by RELAT_1: 36

            .= (p * ( id n)) by FUNCT_2: 61

            .= p by A11, RELAT_1: 51;

            then

             A14: (PP * (perm " )) = ( @ p) by HILB10_2:def 1;

            

             A15: ( eval (T,( @ p))) = ( eval (T,(( @ PP) * (perm " )))) by A14, HILB10_2:def 1

            .= ( eval (Q1,( @ PP))) by HILB10_2: 25

            .= ( eval (P,( @ PPk))) by A5, A13

            .= (a * (p . i1)) by A8;

            

            thus ( eval (TI,( @ (p ^ E)))) = (( eval (t,pE)) - ( eval ((ar * ( 1_1 (i1,FR))),pE))) by POLYNOM2: 24

            .= ( 0. FR) by A10, A15, RLVECT_1: 5

            .= 0 ;

          end;

          given x be n -element XFinSequence of NAT , y be 0 -element XFinSequence of NAT such that

           A16: s = x & ( eval (TI,( @ (x ^ y)))) = 0 ;

          reconsider xy = ( @ (x ^ y)) as Function of n, FR;

          

           A17: ( eval (( 1_1 (i1,FR)),xy)) = (xy . i1) by A3, HILB10_3: 1

          .= (x . i1) by HILB10_2:def 1;

          reconsider Eval = ( eval (( 1_1 (i1,FR)),xy)) as Element of F_Real ;

          

           A18: ( eval ((ar * ( 1_1 (i1,FR))),xy)) = (Ar * Eval) by POLYNOM7: 29

          .= (a * (x . i1)) by A17;

          

           A19: ( dom perm) = n & ( rng perm) = n & ( len x) = n by FUNCT_2: 52, FUNCT_2:def 3, CARD_1:def 7;

          then ( dom (x * perm)) = n by RELAT_1: 27;

          then

          reconsider xp = (x * perm) as XFinSequence by AFINSQ_1: 5;

          

           A20: ( len xp) = n by A19, RELAT_1: 27;

          reconsider XP = xp as n -element XFinSequence of NAT by A20, CARD_1:def 7;

          ( len (XP | k)) = k by A20, A1, AFINSQ_1: 54;

          then

          reconsider XPk = (XP | k) as k -element XFinSequence of NAT by CARD_1:def 7;

          (( @ XP) | k) = (XP | k) by HILB10_2:def 1;

          then

           A21: (( @ XP) | k) = ( @ XPk) by HILB10_2:def 1;

          (XP * (perm " )) = (x * (perm * (perm " ))) by RELAT_1: 36

          .= (x * ( id n)) by FUNCT_2: 61

          .= x by A19, RELAT_1: 51;

          then

           A22: (XP * (perm " )) = ( @ x) by HILB10_2:def 1;

          

           A23: ( eval (T,( @ x))) = ( eval (T,(( @ XP) * (perm " )))) by A22, HILB10_2:def 1

          .= ( eval (Q1,( @ XP))) by HILB10_2: 25

          .= ( eval (P,( @ XPk))) by A5, A21;

          

           A24: (( eval (t,xy)) - ( eval ((ar * ( 1_1 (i1,FR))),xy))) = ( 0. FR) by POLYNOM2: 24, A16;

           P[x] by A24, A18, A23, VECTSP_1: 19;

          hence thesis by A16;

        end;

        hence thesis by HILB10_2:def 6;

      end;

    end;

    theorem :: HILB10_5:14

    

     Th14: for P be INT -valued Polynomial of (k + 1), F_Real , a be Integer, n, i1, i2 st (k + 1) <= n & k in i2 holds { p : for q be (k + 1) -element XFinSequence of NAT st q = ( <%(p . i2)%> ^ (p | k)) holds (a * (p . i1)) = ( eval (P,( @ q))) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let P be INT -valued Polynomial of (k + 1), F_Real , a be Integer, n, i1, i2 such that

       A1: (k + 1) <= n & k in i2;

      set k1 = (k + 1);

      ( dom ( id k)) = k;

      then

      reconsider Idk = ( id k) as XFinSequence by AFINSQ_1: 5;

      

       A2: ( len Idk) = k;

      

       A3: ( rng ( id k)) = ( Segm k);

      then

      reconsider Idk as k -element XFinSequence of NAT by A2, CARD_1:def 7;

      reconsider nk = (n - k1) as Nat by A1, NAT_1: 21;

      set f = ( <%i2%> ^ Idk);

      

       A4: ( rng <%i2%>) = {i2} by AFINSQ_1: 33;

       {i2} misses k by A1, ZFMISC_1: 50;

      then ( rng <%i2%>) misses ( rng Idk) by AFINSQ_1: 33;

      then

       A6: f is one-to-one by CARD_FIN: 52;

      set R = ( rng f);

      

       A7: ( len f) = k1 by CARD_1:def 7;

      

       A8: ( card ( dom f)) = k1 by CARD_1:def 7;

      

       A: k < n by A1, NAT_1: 13;

      then

       A9: ( Segm k) c= ( Segm n) by NAT_1: 39;

      i2 in n by A1, SUBSET_1:def 1;

      then {i2} c= n by ZFMISC_1: 31;

      then (k \/ {i2}) c= n by A9, XBOOLE_1: 8;

      then

       A10: R c= n by AFINSQ_1: 26, A4, A3;

      then ( card (n \ R)) = (( card n) - ( card R)) by CARD_2: 44;

      then

       A11: ( card (n \ R)) = nk by A8, A6, CARD_1: 70;

      

       A12: ( Segm k1) c= ( Segm n) by A1, NAT_1: 39;

      

      then ( card (n \ k1)) = (( card n) - ( card k1)) by CARD_2: 44

      .= nk;

      then

      consider g be Function such that

       A13: g is one-to-one & ( dom g) = (n \ k1) & ( rng g) = (n \ R) by A11, CARD_1: 5, WELLORD2:def 4;

      

       A14: ( rng f) misses ( rng g) & ( dom f) misses ( dom g) by A7, A13, XBOOLE_1: 79;

      then

       A15: (f +* g) is one-to-one by A6, A13, FUNCT_4: 92;

      

       A16: ( dom (f +* g)) = (k1 \/ (n \ k1)) by A7, A13, FUNCT_4:def 1

      .= (k1 \/ n) by XBOOLE_1: 39

      .= n by A12, XBOOLE_1: 12;

      

       A17: ( rng (f +* g)) = (R \/ ( rng g)) by A14, NECKLACE: 6

      .= (n \/ R) by A13, XBOOLE_1: 39

      .= n by A10, XBOOLE_1: 12;

      then

      reconsider fg = (f +* g) as Function of n, n by A16, FUNCT_2: 2;

      ( card n) = ( card n);

      then fg is onto by A15, FINSEQ_4: 63;

      then

      reconsider fg as Permutation of n by A15;

      defpred Q[ XFinSequence of NAT ] means for q be k1 -element XFinSequence of NAT st q = (($1 * fg) | k1) holds (a * ($1 . i1)) = ( eval (P,( @ q)));

      defpred R[ XFinSequence of NAT ] means for q be (k + 1) -element XFinSequence of NAT st q = ( <%($1 . i2)%> ^ ($1 | k)) holds (a * ($1 . i1)) = ( eval (P,( @ q)));

      

       A18: for p be n -element XFinSequence of NAT holds Q[p] iff R[p]

      proof

        let p be n -element XFinSequence of NAT ;

        

         A19: ( len p) = n by CARD_1:def 7;

        then ( dom (p * fg)) = n by A17, A16, RELAT_1: 27;

        then

        reconsider pfg = (p * fg) as XFinSequence by AFINSQ_1: 5;

        set I = <%(p . i2)%>;

        ( len pfg) = n by A19, A17, A16, RELAT_1: 27;

        then

         A20: ( len (pfg | k1)) = k1 by A1, AFINSQ_1: 54;

        

         A21: ( len (p | k)) = k & ( len I) = 1 by AFINSQ_1: 11, A, A19, CARD_1:def 7;

        then

         A22: ( len (I ^ (p | k))) = k1 by AFINSQ_1: 17;

        for i st i in ( dom (I ^ (p | k))) holds ((I ^ (p | k)) . i) = ((pfg | k1) . i)

        proof

          let i;

          assume

           A23: i in ( dom (I ^ (p | k)));

          then

           A24: i in ( dom pfg) & i in k1 & ((pfg | k1) . i) = (pfg . i) by RELAT_1: 57, FUNCT_1: 47, A20, A22;

          then

           A25: (pfg . i) = (p . (fg . i)) & not i in ( dom g) by FUNCT_1: 12, A13, XBOOLE_1: 79, XBOOLE_0: 3;

          then

           A26: (fg . i) = (f . i) by FUNCT_4: 11;

          

           A27: ( len <%i2%>) = 1 by CARD_1:def 7;

          per cases by A23, AFINSQ_1: 20;

            suppose

             A28: i in ( dom I);

            then i < ( len I) = 1 by AFINSQ_1: 66, CARD_1:def 7;

            then i = 0 & i in ( dom <%i2%>) by CARD_1:def 7, A28, NAT_1: 14;

            then (f . i) = ( <%i2%> . i) = i2 & (I . i) = (p . i2) by AFINSQ_1:def 3;

            hence thesis by A24, A25, A26, A28, AFINSQ_1:def 3;

          end;

            suppose ex j st j in ( dom (p | k)) & i = (( len I) + j);

            then

            consider j such that

             A29: j in ( dom (p | k)) & i = (( len I) + j);

            

             A30: ((I ^ (p | k)) . i) = ((p | k) . j) = (p . j) by A29, AFINSQ_1:def 3, FUNCT_1: 47;

            j in ( dom Idk) by A, A19, A29, AFINSQ_1: 11;

            then (f . i) = (Idk . j) = j by A21, A27, A29, AFINSQ_1:def 3, FUNCT_1: 17;

            hence thesis by A30, A24, A25, FUNCT_4: 11;

          end;

        end;

        hence thesis by A20, A22, AFINSQ_1: 8;

      end;

      { p : Q[p] } = { q : R[q] } from HILB10_3:sch 2( A18);

      hence thesis by Th13, A1;

    end;

    theorem :: HILB10_5:15

    

     Th15: for P be INT -valued Polynomial of (k + 1), F_Real , n, i1, i2 st (k + 1) <= n & k in i1 holds { p : for q be (k + 1) -element XFinSequence of NAT st q = ( <%(p . i1)%> ^ (p | k)) holds (( eval (P,( @ q))), 0 ) are_congruent_mod (p . i2) } is diophantine Subset of (n -xtuples_of NAT )

    proof

      set k1 = (k + 1);

      let P be INT -valued Polynomial of k1, F_Real , n, i1, i2 such that

       A1: (k + 1) <= n & k in i1;

      reconsider FR = F_Real as Field;

      set X = (n + 1);

      

       A2: n < X & k < n by A1, NAT_1: 13;

      then n in ( Segm X) by NAT_1: 44;

      then

      reconsider N = n, I1 = i1, I2 = i2 as Element of X by HILB10_3: 2;

      defpred P[ XFinSequence of NAT ] means ((1 * ($1 . N)),( 0 * ($1 . I1))) are_congruent_mod (1 * ($1 . I2));

      

       A3: { p where p be X -element XFinSequence of NAT : P[p] } is diophantine Subset of (X -xtuples_of NAT ) by HILB10_3: 21;

      defpred QP[ XFinSequence of NAT ] means for q be k1 -element XFinSequence of NAT st q = ( <%($1 . I1)%> ^ ($1 | k)) holds (1 * ($1 . N)) = ( eval (P,( @ q)));

      defpred QM[ XFinSequence of NAT ] means for q be k1 -element XFinSequence of NAT st q = ( <%($1 . I1)%> ^ ($1 | k)) holds (( - 1) * ($1 . N)) = ( eval (P,( @ q)));

      defpred Q[ XFinSequence of NAT ] means QP[$1] or QM[$1];

      

       A4: k1 < X & k in I1 by A1, NAT_1: 13;

      then

       A5: { p where p be X -element XFinSequence of NAT : QP[p] } is diophantine Subset of (X -xtuples_of NAT ) by Th14;

      

       A6: { p where p be X -element XFinSequence of NAT : QM[p] } is diophantine Subset of (X -xtuples_of NAT ) by Th14, A4;

      { p where p be X -element XFinSequence of NAT : QP[p] or QM[p] } is diophantine Subset of (X -xtuples_of NAT ) from HILB10_3:sch 1( A5, A6);

      then

       A7: { p where p be X -element XFinSequence of NAT : Q[p] } is diophantine Subset of (X -xtuples_of NAT );

      set PQ = { p where p be X -element XFinSequence of NAT : P[p] & Q[p] };

      

       A8: PQ is diophantine Subset of (X -xtuples_of NAT ) from HILB10_3:sch 3( A3, A7);

      set PQr = { (p | n) where p be X -element XFinSequence of NAT : p in PQ };

      defpred S[ XFinSequence of NAT ] means for q be k1 -element XFinSequence of NAT st q = ( <%($1 . i1)%> ^ ($1 | k)) holds (( eval (P,( @ q))), 0 ) are_congruent_mod ($1 . i2);

      set S = { p : S[p] };

      

       A9: PQr is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 5, A2, A8;

      

       A10: ( Segm k) c= ( Segm n) by A2, NAT_1: 39;

      

       A11: S c= PQr

      proof

        let y be object;

        assume y in S;

        then

        consider p such that

         A12: y = p & S[p];

        

         A13: ( len p) = n & ( len <%(p . i1)%>) = 1 by CARD_1:def 7;

        then ( len (p | k)) = k by A2, AFINSQ_1: 54;

        then ( len ( <%(p . i1)%> ^ (p | k))) = k1 by A13, AFINSQ_1: 17;

        then

        reconsider pi1pk = ( <%(p . i1)%> ^ (p | k)) as k1 -element XFinSequence of NAT by CARD_1:def 7;

        reconsider E = |.( eval (P,( @ pi1pk))).| as Element of NAT ;

        reconsider pE = (p ^ <%E%>) as X -element XFinSequence of NAT ;

        

         A14: (pE | n) = p by A13, AFINSQ_1: 57;

        

         A15: (pE . N) = E by A13, AFINSQ_1: 36;

        

         A16: (pE . I1) = (p . i1) & (pE . I2) = (p . i2) by A1, A14, HILB10_3: 4;

        

         A17: (pE | k) = (p | k) by A10, A14, RELAT_1: 74;

         A18:

        now

          per cases by ABSVALUE: 1;

            suppose E = ( eval (P,( @ pi1pk)));

            hence QP[pE] or QM[pE] by A13, AFINSQ_1: 36, A17, A16;

          end;

            suppose E = ( - ( eval (P,( @ pi1pk))));

            hence QP[pE] or QM[pE] by A15, A10, A14, RELAT_1: 74, A16;

          end;

        end;

        (( eval (P,( @ pi1pk))), 0 ) are_congruent_mod (pE . i2) by A12, A16;

        then

         A19: (pE . i2) divides ( - (( eval (P,( @ pi1pk))) - 0 )) by INT_2: 10, INT_2: 15;

        ((1 * (pE . N)),( 0 * (pE . I1))) are_congruent_mod (1 * (pE . I2))

        proof

          per cases by ABSVALUE: 1;

            suppose E = ( eval (P,( @ pi1pk)));

            hence thesis by A12, A16, A15;

          end;

            suppose E = ( - ( eval (P,( @ pi1pk))));

            then (pE . i2) divides (E - ( - 0 )) by A19;

            hence thesis by A15, INT_2: 15;

          end;

        end;

        then pE in PQ by A18;

        hence thesis by A12, A14;

      end;

      PQr c= S

      proof

        let y be object;

        assume y in PQr;

        then

        consider pP be X -element XFinSequence of NAT such that

         A20: y = (pP | n) & pP in PQ;

        

         A21: ex q be X -element XFinSequence of NAT st q = pP & P[q] & Q[q] by A20;

        ( len pP) = X by CARD_1:def 7;

        then

         A22: ( len (pP | n)) = n by A2, AFINSQ_1: 54;

        then

        reconsider p = (pP | n) as n -element XFinSequence of NAT by CARD_1:def 7;

        

         A23: ( len <%(p . i1)%>) = 1 by CARD_1:def 7;

        ( len (p | k)) = k by A2, A22, AFINSQ_1: 54;

        then ( len ( <%(p . i1)%> ^ (p | k))) = k1 by A23, AFINSQ_1: 17;

        then

        reconsider pi1pk = ( <%(p . i1)%> ^ (p | k)) as k1 -element XFinSequence of NAT by CARD_1:def 7;

        

         A24: (pP . I1) = (p . i1) & (pP . I2) = (p . i2) by A1, HILB10_3: 4;

        

         A25: (pP . I2) divides ((pP . N) - 0 ) by A21, INT_2: 15;

        (( eval (P,( @ pi1pk))), 0 ) are_congruent_mod (p . i2)

        proof

          pi1pk = ( <%(pP . i1)%> ^ (pP | k)) by A24, A10, RELAT_1: 74;

          then (1 * (pP . N)) = ( eval (P,( @ pi1pk))) or (( - 1) * (pP . N)) = ( eval (P,( @ pi1pk))) by A21;

          per cases ;

            suppose (pP . N) = ( eval (P,( @ pi1pk)));

            hence thesis by A21, A1, HILB10_3: 4;

          end;

            suppose

             A26: (pP . N) = ( - ( eval (P,( @ pi1pk))));

            (p . i2) divides (( - (pP . N)) - 0 ) by A25, INT_2: 10, A24;

            hence thesis by A26, INT_2: 15;

          end;

        end;

        then S[p];

        hence thesis by A20;

      end;

      hence thesis by A9, A11, XBOOLE_0:def 10;

    end;

    begin

    theorem :: HILB10_5:16

    

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

    proof

      let p be INT -valued Polynomial of ((2 + n) + k), F_Real , X be n -element XFinSequence of NAT , x be Element of NAT ;

      set x1 = (x + 1);

      thus (for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 ) implies ex Y be k -element XFinSequence of NAT , Z,e,K be Element of NAT st K > x & K >= (( sum_of_coefficients |.p.|) * (((((x ^2 ) + 1) * ( Product (1 + X))) * e) |^ ( degree p))) & (for i be 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 be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq e)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))))

      proof

        assume

         A1: for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 ;

        defpred P[ object, object] means $1 in NAT & $2 is k -element XFinSequence of NAT & for z be Element of NAT , y be k -element XFinSequence of NAT st z = $1 & y = $2 holds ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 ;

        

         A2: for i be Nat st i in x1 holds ex g be object st P[i, g]

        proof

          let i be Nat;

          assume i in x1;

          then

           A3: i in ( Segm x1);

          reconsider z = i as Element of NAT by ORDINAL1:def 12;

          i < x1 by A3, NAT_1: 44;

          then i <= x by NAT_1: 13;

          then

          consider y be k -element XFinSequence of NAT such that

           A4: ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 by A1;

          take y;

          thus thesis by A4, ORDINAL1:def 12;

        end;

        consider YY be XFinSequence such that

         A5: ( dom YY) = x1 & for i be Nat st i in (x + 1) holds P[i, (YY . i)] from AFINSQ_1:sch 1( A2);

        YY is XFinSequence-yielding by A5;

        then

        reconsider YY as XFinSequence-yielding XFinSequence;

        defpred Q[ object, object] means not contradiction;

        set M = { ((YY . i) . j) where i,j be Nat : Q[i, j] };

        

         A6: M is finite from SCH1;

        

         A7: M is natural-membered

        proof

          let x be object;

          assume x in M;

          then

          consider i,j be Nat such that

           A8: x = ((YY . i) . j) & Q[i, j];

          per cases ;

            suppose i in ( dom YY);

            then P[i, (YY . i)] by A5;

            hence x is natural by A8;

          end;

            suppose not i in ( dom YY);

            then (YY . i) = {} by FUNCT_1:def 2;

            hence thesis by A8;

          end;

        end;

        then

        reconsider Mx = (M \/ {x, 1}) as non empty natural-membered finite set by A6;

        set e = (1 + ( max Mx));

        set K = ((x1 + e) + (( sum_of_coefficients |.p.|) * (((((x ^2 ) + 1) * ( Product (1 + X))) * e) |^ ( degree p))));

        set h = (1 + ((K ! ) * ( idseq x1)));

        

         A9: ( len h) = x1 by CARD_1:def 7;

        

         A10: for i st i in ( dom h) holds (h . i) = (((K ! ) * i) + 1)

        proof

          let i such that

           A11: i in ( dom h);

          

           A12: ( dom h) = ( dom ((K ! ) * ( idseq x1))) = ( dom ( idseq x1)) by VALUED_1:def 2, VALUED_1:def 5;

          

          thus (h . i) = (1 + (((K ! ) * ( idseq x1)) . i)) by A11, VALUED_1:def 2

          .= (1 + ((K ! ) * (( idseq x1) . i))) by A11, A12, VALUED_1:def 5

          .= (((K ! ) * i) + 1) by A11, A12, FINSEQ_2: 49;

        end;

        

         A13: (x1 + e) <= K & x1 <= (x1 + e) & e <= (x1 + e) by NAT_1: 11;

        then

         A14: K >= x1 > 0 by XXREAL_0: 2;

        then

        reconsider h 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) <= x1 by NAT_1: 13;

        then (h . 1) divides ( Product h) & (h . 1) = (((K ! ) * 1) + 1) by A10, A15, INT_4: 32, A9, FINSEQ_3: 25;

        then (h . 1) <= ( Product h) & (h . 1) > (K ! ) by INT_2: 27, NAT_1: 13;

        then K <= (K ! ) & (K ! ) < ( Product h) by XXREAL_0: 2, NEWTON: 38;

        then e <= K & K < ( Product h) by A13, XXREAL_0: 2;

        then

         A16: e < ( Product h) by XXREAL_0: 2;

        defpred Q[ object, object] means $1 in NAT & $2 in NAT & for i,z be Nat st i = $1 & z = $2 holds e < z & for j,F be Nat st j in x1 & F = ((YY . j) . i) holds (z,F) are_congruent_mod (h . (j + 1));

        

         A17: for i be Nat st i in k holds ex Y be object st Q[i, Y]

        proof

          let i be Nat such that i in k;

          deffunc H( Nat) = ((YY . ($1 -' 1)) . i);

          consider X be FinSequence such that

           A18: ( len X) = x1 & for k be 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;

            assume y in ( rng X);

            then

            consider x be object such that

             A19: x in ( dom X) & (X . x) = y by FUNCT_1:def 3;

            reconsider x as Nat by A19;

            (X . x) = ((YY . (x -' 1)) . i) by A18, A19;

            then (X . x) in M;

            then (X . x) is natural by A7;

            hence thesis by A19;

          end;

          then

          reconsider X as FinSequence of NAT by FINSEQ_1:def 4;

          consider z be Integer such that

           A20: 0 <= z & z < ( Product h) and

           A21: for i be 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));

          thus i in NAT & Y in NAT by A20, ORDINAL1:def 12;

          let I,Z be Nat such that

           A22: I = i & Z = Y;

          Y >= ( Product h) by A20, NAT_1: 11;

          hence e < Z by A22, A16, XXREAL_0: 2;

          let j,F be Nat such that

           A23: j in x1 & F = ((YY . j) . I);

          x1 = ( Segm x1);

          then j < x1 by A23, NAT_1: 44;

          then

           A24: 1 <= (j + 1) <= x1 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 thesis by A26, A23, A22, NAT_D: 34;

        end;

        consider YC be XFinSequence such that

         A27: ( dom YC) = k & for i be Nat st i in k holds Q[i, (YC . i)] from AFINSQ_1:sch 1( A17);

        ( rng YC) c= NAT

        proof

          let y be object;

          assume y in ( rng YC);

          then ex x be object st x in ( dom YC) & (YC . x) = y by FUNCT_1:def 3;

          hence thesis by A27;

        end;

        then

        reconsider YC as k -element XFinSequence of NAT by A27, CARD_1:def 7, RELAT_1:def 19;

        consider Z be Nat such that

         A29: ( Product (1 + ((K ! ) * ( idseq x1)))) = (1 + ((K ! ) * Z)) & (x1 > 0 implies Z > 0 ) by Lm1;

        reconsider Z1 = (Z - 1) as Element of NAT by NAT_1: 20, A29;

        reconsider e, K as Element of NAT by ORDINAL1:def 12;

        take YC, Z1, e, K;

        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;

        thus for i be Nat st i in k holds (YC . i) > e by A27;

        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;

        thus (1 + ((Z1 + 1) * (K ! ))) = ( Product (1 + ((K ! ) * ( idseq x1)))) by A29;

        

         A30: for b,c be 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 be Element of NAT st b in ( dom h) holds (h . b) divides E

        proof

          let b be Element of NAT such that

           A32: b in ( dom h);

          

           A33: (h . b) = (((K ! ) * b) + 1) by A32, A10;

          1 <= b <= x1 by A9, A32, FINSEQ_3: 25;

          then

          reconsider b1 = (b - 1) as Element of NAT by NAT_1: 21;

          (b1 + 1) <= x1 by A9, A32, FINSEQ_3: 25;

          then b1 < ( Segm x1) by NAT_1: 13;

          then

           A34: b1 in x1 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 st i in ((2 + n) + k) holds (h . b) divides (((( <%Z1, x%> ^ X) ^ YC) . i) - ((( <%b1, x%> ^ X) ^ YYb) . i))

          proof

            let i;

            

             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 = ( len YYb) by CARD_1:def 7;

            assume i in ((2 + n) + k);

            per cases by A36, AFINSQ_1: 20;

              suppose

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

              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%>);

                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 ;

                  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 x1)))) - (h . b)) by A29, A33;

                  (h . b) divides ((Z1 - b1) * (K ! )) by A48, A49, INT_5: 1;

                  hence thesis by A45, A47, A46, INT_2:def 3, A33, INT_2: 25;

                end;

                  suppose i = 1;

                  hence thesis by INT_2: 12, A41, A44;

                end;

              end;

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

                then

                consider j 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 thesis by A41, INT_2: 12;

              end;

            end;

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

              then

              consider j 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 thesis by A52, A53, INT_1:def 4;

            end;

          end;

          then (h . b) divides (E - 0 ) by A32, A35, Th1;

          hence thesis;

        end;

        ( Product h) divides E

        proof

          per cases ;

            suppose E >= 0 ;

            hence thesis by A30, A31, A15, INT_4: 38;

          end;

            suppose E < 0 ;

            then

            reconsider mE = ( - E) as Element of NAT by INT_1: 3;

            for b be Element of NAT st b in ( dom h) holds (h . b) divides mE by A31, INT_2: 10;

            hence thesis by INT_2: 10, A30, A15, INT_4: 38;

          end;

        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;

        let i be Nat such that

         A54: i in k;

        set YCe = (((YC . i) + 1) + ( - ( idseq e)));

        

         A55: ( dom YCe) = ( dom ( - ( idseq e))) = ( dom ( idseq e)) by VALUED_1:def 2, VALUED_1: 8;

        

         A56: for j st j in ( dom YCe) holds (YCe . j) = (((YC . i) + 1) - j)

        proof

          let j such that

           A57: j in ( dom YCe);

          

          thus (YCe . 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);

        end;

        ( rng YCe) c= NAT

        proof

          let b be Integer;

          assume b in ( rng YCe);

          then

          consider a be object such that

           A58: a in ( dom YCe) & (YCe . a) = b by FUNCT_1:def 3;

          reconsider a as Nat by A58;

          

           A59: (YCe . a) = (((YC . i) + 1) - a) by A56, A58;

          (YC . i) > 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 thesis by A58, A59, ORDINAL1:def 12;

        end;

        then

        reconsider YCe as FinSequence of NAT by FINSEQ_1:def 4;

        reconsider PP = ( Product YCe) as Element of NAT ;

        

         A60: for b be Element of NAT st b in ( dom h) holds (h . b) divides PP

        proof

          let b be Element of NAT such that

           A61: b in ( dom h);

          1 <= b <= x1 by A61, A9, FINSEQ_3: 25;

          then

          reconsider b1 = (b - 1) as Nat;

          

           A62: ((YY . b1) . i) in M;

          then

          reconsider YYb1i = ((YY . b1) . i) as Nat by A7;

          (b1 + 1) <= x1 by A61, A9, FINSEQ_3: 25;

          then b1 < ( Segm x1) by NAT_1: 13;

          then b1 in x1 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) <= 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 thesis by A65, A63, INT_2: 9;

        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;

      end;

      given Y be k -element XFinSequence of NAT , Z,e,K be 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 be 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 be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq e)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! )));

      let z be Element of NAT such that

       A70: z <= x;

      set z1 = (z + 1), K1 = (K ! ), ZZ = (1 + ((z + 1) * K1));

      

       A71: ZZ > (1 + 0 ) by XREAL_1: 8;

      consider prim be Element of NAT such that

       A72: prim divides ZZ & prim <= ZZ & prim is prime by A71, NAT_4: 13;

      deffunc P( object) = ((Y . $1) mod prim);

      consider Yz be XFinSequence such that

       A73: ( len Yz) = k & for i be Nat st i in k holds (Yz . i) = P(i) from AFINSQ_1:sch 2;

      ( rng Yz) c= NAT

      proof

        let y be object;

        assume y in ( rng Yz);

        then

        consider x be object such that

         A74: x in ( dom Yz) & (Yz . x) = y by FUNCT_1:def 3;

        y = P(x) by A73, A74;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider Yz as k -element XFinSequence of NAT by A73, RELAT_1:def 19, CARD_1:def 7;

      1 <= z1 <= x1 by A70, NAT_1: 11, XREAL_1: 6;

      then

       A75: z1 in ( Seg x1);

      K >= x1 by A66, NAT_1: 13;

      then

      reconsider h = (1 + (K1 * ( idseq x1))) 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 (K1 * ( idseq (x + 1)))) = ( dom ( idseq (x + 1))) by VALUED_1:def 2, VALUED_1:def 5;

      

       A78: (h . z1) = (1 + ((K1 * ( idseq (x + 1))) . z1)) by A75, A77, VALUED_1:def 2

      .= (1 + (K1 * (( idseq (x + 1)) . z1))) by A75, A77, VALUED_1:def 5

      .= ZZ by A75, FINSEQ_2: 49;

      ZZ divides (1 + ((Z + 1) * K1)) by A78, A68, A76, INT_4: 32, A75, A77;

      then

       A79: prim divides (1 + ((Z + 1) * K1)) by A72, INT_2: 9;

      (1 + ((Z + 1) * K1)) 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;

        then prim divides ((Z + 1) * K1) by INT_2: 2, A72, NEWTON: 41;

        then prim divides 1 by A79, INT_2: 1;

        then prim = 1 by INT_2: 13;

        hence thesis by A72, INT_2:def 4;

      end;

      

       A82: ( len <%z, x%>) = 2 = ( len <%Z, x%>) by CARD_1:def 7;

      

       A83: ( len ( <%z, x%> ^ X)) = (2 + n) = ( len ( <%Z, x%> ^ X)) by CARD_1:def 7;

      

       A84: ( len Y) = k = ( len Yz) by CARD_1:def 7;

      

       A85: ( len (( <%z, x%> ^ X) ^ Yz)) = ((2 + k) + n) by CARD_1:def 7;

      for i st i in ((2 + k) + n) holds prim divides (((( <%Z, x%> ^ X) ^ Y) . i) - ((( <%z, x%> ^ X) ^ Yz) . i))

      proof

        let i such that

         A86: i in ((2 + k) + n);

        per cases by A86, A85, AFINSQ_1: 20;

          suppose

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

          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%>);

            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 ;

              then

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

              

               A91: (K1,prim) are_coprime

              proof

                assume not (K1,prim) are_coprime ;

                then

                 A92: (K1 gcd prim) <> 1 by INT_2:def 3;

                (K1 gcd prim) divides prim by INT_2:def 2;

                then (K1 gcd prim) = prim by A92, A72, INT_2:def 4;

                then prim divides K1 by INT_2:def 2;

                hence thesis by A81, NAT_4: 19, A72;

              end;

              prim divides ((1 + ((Z + 1) * K1)) - (1 + ((z + 1) * K1))) by A79, A72, INT_5: 1;

              then prim divides ((Z - z) * K1);

              hence thesis by A90, A91, INT_2: 25;

            end;

              suppose i = 1;

              hence thesis by A88, A89, INT_2: 12;

            end;

          end;

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

            then

            consider j 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 thesis by INT_2: 12, A88;

          end;

        end;

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

          then

          consider j 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 thesis by A95, A72, PEPIN: 8;

        end;

      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 be 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 be 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;

        assume i in ( dom ( @ (( <%z, x%> ^ X) ^ Yz)));

        then

         A98: i in ( dom (( <%z, x%> ^ X) ^ Yz)) & (( <%z, x%> ^ X) ^ Yz) = ( @ (( <%z, x%> ^ X) ^ Yz)) by HILB10_2:def 1;

        reconsider i as Nat by A98;

        per cases by A98, AFINSQ_1: 20;

          suppose

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

          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%>);

            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 ;

              hence thesis by A103, A70, XXREAL_0: 2, A100, A101;

            end;

              suppose i = 1;

              hence thesis by A103, A100, A101;

            end;

          end;

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

            then

            consider j 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 thesis by A104, AFINSQ_1:def 3, A100;

          end;

        end;

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

          then

          consider j 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) * K1)) divides (( Product YE) - 0 ) by INT_1:def 4, A69, A108, A73;

          

           A112: ( len YE) = ( len ( idseq e)) = e by CARD_1:def 7;

          

           A113: for w be Nat st w in ( dom YE) holds ((((Y . j) + 1) + ( - ( idseq e))) . w) = (((Y . j) + 1) - w)

          proof

            let w be Nat;

            assume

             A114: w in ( dom YE);

            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 (YE . w) = (((Y . j) + 1) + ( - w)) by A114, VALUED_1:def 2;

            hence thesis;

          end;

           A115:

          now

            let a be Nat;

            assume

             A116: a in ( dom YE);

            1 <= 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;

            (YE . a) = (((Y . j) + 1) - a) by A116, A113;

            then ((YE . a) + a1) > e by A67, A84, A108;

            hence (YE . a) > 0 by A117, XREAL_1: 19;

          end;

          now

            let r be object;

            assume r in ( rng YE);

            then

            consider a be object such that

             A118: a in ( dom YE) & (YE . a) = r by FUNCT_1:def 3;

            reconsider a as Nat by A118;

            (YE . a) > 0 by A115, A118;

            hence r in NAT by A118, INT_1: 3;

          end;

          then

           A119: YE is FinSequence of NAT by FINSEQ_1:def 4, TARSKI:def 3;

          YE is positive-yielding

          proof

            let r be Real;

            assume r in ( rng YE);

            then

            consider a be object such that

             A120: a in ( dom YE) & (YE . a) = r by FUNCT_1:def 3;

            thus thesis by A115, A120;

          end;

          then

          consider w be Nat such that

           A121: w in ( dom YE) & prim divides (YE . w) by A111, A79, INT_2: 9, Th12, A72, A119;

          

           A122: 1 <= 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 thesis by A109, A98;

        end;

      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 thesis;

    end;

    theorem :: HILB10_5:17

    

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

    proof

      let p be INT -valued Polynomial of ((2 + n) + k), F_Real , X be n -element XFinSequence of NAT , x be Element of NAT ;

      set x1 = (x + 1);

      thus (for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 ) implies ex Y be k -element XFinSequence of NAT , Z,K be Element of NAT st K > x & K >= (( sum_of_coefficients |.p.|) * ((((x ^2 ) + 1) * ( Product (1 + X))) |^ ( degree p))) & (for i be Nat st i in k holds (Y . i) > x1) & (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 be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq x1)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))))

      proof

        assume

         A1: for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 ;

        defpred P[ object, object] means $1 in NAT & $2 is k -element XFinSequence of NAT & for z be Element of NAT , y be k -element XFinSequence of NAT st z = $1 & y = $2 holds (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 ;

        

         A2: for i be Nat st i in x1 holds ex g be object st P[i, g]

        proof

          let i be Nat;

          assume i in x1;

          then

           A3: i in ( Segm x1);

          reconsider z = i as Element of NAT by ORDINAL1:def 12;

          i < x1 by A3, NAT_1: 44;

          then i <= x by NAT_1: 13;

          then

          consider y be k -element XFinSequence of NAT such that

           A4: for i st i in k holds (y . i) <= x and

           A5: ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 by A1;

          take y;

          thus thesis by A4, A5, ORDINAL1:def 12;

        end;

        consider YY be XFinSequence such that

         A6: ( dom YY) = x1 & for i be Nat st i in (x + 1) holds P[i, (YY . i)] from AFINSQ_1:sch 1( A2);

        YY is XFinSequence-yielding by A6;

        then

        reconsider YY as XFinSequence-yielding XFinSequence;

        defpred Q[ object, object] means not contradiction;

        set M = { ((YY . i) . j) where i,j be Nat : Q[i, j] };

        

         A7: M is finite from SCH1;

        

         A8: M is natural-membered

        proof

          let x be object;

          assume x in M;

          then

          consider i,j be Nat such that

           A9: x = ((YY . i) . j) & Q[i, j];

          per cases ;

            suppose i in ( dom YY);

            then P[i, (YY . i)] by A6;

            hence x is natural by A9;

          end;

            suppose not i in ( dom YY);

            then (YY . i) = {} by FUNCT_1:def 2;

            hence thesis by A9;

          end;

        end;

        then

        reconsider Mx = (M \/ {x, 1}) as non empty natural-membered finite set by A7;

        set K = (x1 + (( sum_of_coefficients |.p.|) * ((((x ^2 ) + 1) * ( Product (1 + X))) |^ ( degree p))));

        set h = (1 + ((K ! ) * ( idseq x1)));

        

         A10: ( len h) = x1 by CARD_1:def 7;

        

         A11: for i st i in ( dom h) holds (h . i) = (((K ! ) * i) + 1)

        proof

          let i such that

           A12: i in ( dom h);

          

           A13: ( dom h) = ( dom ((K ! ) * ( idseq x1))) = ( dom ( idseq x1)) by VALUED_1:def 2, VALUED_1:def 5;

          

          thus (h . i) = (1 + (((K ! ) * ( idseq x1)) . i)) by A12, VALUED_1:def 2

          .= (1 + ((K ! ) * (( idseq x1) . i))) by A12, A13, VALUED_1:def 5

          .= (((K ! ) * i) + 1) by A12, A13, FINSEQ_2: 49;

        end;

        

         A14: K >= x1 > 0 by NAT_1: 11;

        reconsider h as CR_Sequence by NAT_1: 11, Th2;

        ( rng h) c= NAT by VALUED_0:def 6;

        then

         A15: h is FinSequence of NAT by FINSEQ_1:def 4;

        ( 0 + 1) <= x1 by NAT_1: 13;

        then (h . 1) divides ( Product h) & (h . 1) = (((K ! ) * 1) + 1) by A11, A15, INT_4: 32, A10, FINSEQ_3: 25;

        then (h . 1) <= ( Product h) & (h . 1) > (K ! ) by INT_2: 27, NAT_1: 13;

        then K <= (K ! ) & (K ! ) < ( Product h) by XXREAL_0: 2, NEWTON: 38;

        then x1 <= K & K < ( Product h) by NAT_1: 11, XXREAL_0: 2;

        then

         A16: x1 < ( Product h) by XXREAL_0: 2;

        defpred Q[ object, object] means $1 in NAT & $2 in NAT & for i,z be Nat st i = $1 & z = $2 holds x1 < z & for j,F be Nat st j in x1 & F = ((YY . j) . i) holds (z,F) are_congruent_mod (h . (j + 1));

        

         A17: for i be Nat st i in k holds ex Y be object st Q[i, Y]

        proof

          let i be Nat such that i in k;

          deffunc H( Nat) = ((YY . ($1 -' 1)) . i);

          consider X be FinSequence such that

           A18: ( len X) = x1 & for k be 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;

            assume y in ( rng X);

            then

            consider x be object such that

             A19: x in ( dom X) & (X . x) = y by FUNCT_1:def 3;

            reconsider x as Nat by A19;

            (X . x) = ((YY . (x -' 1)) . i) by A18, A19;

            then (X . x) in M;

            then (X . x) is natural by A8;

            hence thesis by A19;

          end;

          then

          reconsider X as FinSequence of NAT by FINSEQ_1:def 4;

          consider z be Integer such that

           A20: 0 <= z & z < ( Product h) and

           A21: for i be Nat st i in ( dom X) holds (z,(X . i)) are_congruent_mod (h . i) by INT_6: 41, A18, A10;

          take Y = (z + ( Product h));

          thus i in NAT & Y in NAT by A20, ORDINAL1:def 12;

          let I,Z be Nat such that

           A22: I = i & Z = Y;

          Y >= ( Product h) by A20, NAT_1: 11;

          hence x1 < Z by A22, A16, XXREAL_0: 2;

          let j,F be Nat such that

           A23: j in x1 & F = ((YY . j) . I);

          x1 = ( Segm x1);

          then j < x1 by A23, NAT_1: 44;

          then

           A24: 1 <= (j + 1) <= x1 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, A10, 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 thesis by A26, A23, A22, NAT_D: 34;

        end;

        consider YC be XFinSequence such that

         A27: ( dom YC) = k & for i be Nat st i in k holds Q[i, (YC . i)] from AFINSQ_1:sch 1( A17);

        ( rng YC) c= NAT

        proof

          let y be object;

          assume y in ( rng YC);

          then ex x be object st x in ( dom YC) & (YC . x) = y by FUNCT_1:def 3;

          hence thesis by A27;

        end;

        then

        reconsider YC as k -element XFinSequence of NAT by A27, CARD_1:def 7, RELAT_1:def 19;

        consider Z be Nat such that

         A29: ( Product (1 + ((K ! ) * ( idseq x1)))) = (1 + ((K ! ) * Z)) & (x1 > 0 implies Z > 0 ) by Lm1;

        reconsider Z1 = (Z - 1) as Element of NAT by NAT_1: 20, A29;

        reconsider K as Element of NAT by ORDINAL1:def 12;

        take YC, Z1, K;

        thus K > x & K >= (( sum_of_coefficients |.p.|) * ((((x ^2 ) + 1) * ( Product (1 + X))) |^ ( degree p))) by NAT_1: 11, NAT_1: 13, A14;

        thus for i be Nat st i in k holds (YC . i) > x1 by A27;

        thus (1 + ((Z1 + 1) * (K ! ))) = ( Product (1 + ((K ! ) * ( idseq x1)))) by A29;

        

         A30: for b,c be 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 be Element of NAT st b in ( dom h) holds (h . b) divides E

        proof

          let b be Element of NAT such that

           A32: b in ( dom h);

          

           A33: (h . b) = (((K ! ) * b) + 1) by A32, A11;

          1 <= b <= x1 by A10, A32, FINSEQ_3: 25;

          then

          reconsider b1 = (b - 1) as Element of NAT by NAT_1: 21;

          (b1 + 1) <= x1 by A10, A32, FINSEQ_3: 25;

          then b1 < ( Segm x1) by NAT_1: 13;

          then

           A34: b1 in x1 by NAT_1: 44;

          then

          reconsider YYb = (YY . b1) as k -element XFinSequence of NAT by A6;

          

           A35: ( eval (p,( @ (( <%b1, x%> ^ X) ^ YYb)))) = 0 by A34, A6;

          for i st i in ((2 + n) + k) holds (h . b) divides (((( <%Z1, x%> ^ X) ^ YC) . i) - ((( <%b1, x%> ^ X) ^ YYb) . i))

          proof

            let i;

            

             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 = ( len YYb) by CARD_1:def 7;

            assume i in ((2 + n) + k);

            per cases by A36, AFINSQ_1: 20;

              suppose

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

              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%>);

                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 ;

                  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 x1)))) - (h . b)) by A29, A33;

                  (h . b) divides ((Z1 - b1) * (K ! )) by A48, A49, INT_5: 1;

                  hence thesis by A45, A47, INT_2: 25, A46, INT_2:def 3, A33;

                end;

                  suppose i = 1;

                  hence thesis by INT_2: 12, A41, A44;

                end;

              end;

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

                then

                consider j 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 thesis by A41, INT_2: 12;

              end;

            end;

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

              then

              consider j 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 thesis by A52, A53, INT_1:def 4;

            end;

          end;

          then (h . b) divides (E - 0 ) by A32, A35, Th1;

          hence thesis;

        end;

        ( Product h) divides E

        proof

          per cases ;

            suppose E >= 0 ;

            hence thesis by A30, A31, A15, INT_4: 38;

          end;

            suppose E < 0 ;

            then

            reconsider mE = ( - E) as Element of NAT by INT_1: 3;

            for b be Element of NAT st b in ( dom h) holds (h . b) divides mE by A31, INT_2: 10;

            hence thesis by INT_2: 10, A30, A15, INT_4: 38;

          end;

        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;

        let i be Nat such that

         A54: i in k;

        set YCe = (((YC . i) + 1) + ( - ( idseq x1)));

        

         A55: ( dom YCe) = ( dom ( - ( idseq x1))) = ( dom ( idseq x1)) by VALUED_1:def 2, VALUED_1: 8;

        

         A56: for j st j in ( dom YCe) holds (YCe . j) = (((YC . i) + 1) - j)

        proof

          let j such that

           A57: j in ( dom YCe);

          

          thus (YCe . j) = (((YC . i) + 1) + (( - ( idseq x1)) . j)) by A57, VALUED_1:def 2

          .= (((YC . i) + 1) + ( - (( idseq x1) . j))) by VALUED_1: 8

          .= (((YC . i) + 1) + ( - j)) by A57, A55, FINSEQ_2: 49

          .= (((YC . i) + 1) - j);

        end;

        ( rng YCe) c= NAT

        proof

          let b be Integer;

          assume b in ( rng YCe);

          then

          consider a be object such that

           A58: a in ( dom YCe) & (YCe . a) = b by FUNCT_1:def 3;

          reconsider a as Nat by A58;

          

           A59: (YCe . a) = (((YC . i) + 1) - a) by A56, A58;

          (YC . i) > x1 >= 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 thesis by A58, A59, ORDINAL1:def 12;

        end;

        then

        reconsider YCe as FinSequence of NAT by FINSEQ_1:def 4;

        reconsider PP = ( Product YCe) as Element of NAT ;

        

         A60: for b be Element of NAT st b in ( dom h) holds (h . b) divides PP

        proof

          let b be Element of NAT such that

           A61: b in ( dom h);

          1 <= b <= x1 by A61, A10, FINSEQ_3: 25;

          then

          reconsider b1 = (b - 1) as Nat;

          ((YY . b1) . i) in M;

          then

          reconsider YYb1i = ((YY . b1) . i) as Nat by A8;

          (b1 + 1) <= x1 by A61, A10, FINSEQ_3: 25;

          then b1 < ( Segm x1) by NAT_1: 13;

          then

           A62: b1 in x1 by NAT_1: 44;

          then P[b1, (YY . b1)] by A6;

          then

           A63: YYb1i <= x by A54;

          ((YC . i),YYb1i) are_congruent_mod (h . (b1 + 1)) by A62, A27, A54;

          then

           A64: (h . b) divides ((YC . i) - YYb1i) by INT_1:def 4;

          ( 0 + 1) <= (YYb1i + 1) <= x1 by A63, XREAL_1: 7;

          then

           A65: (YYb1i + 1) in ( dom YCe) by A55;

          then

           A66: (YCe . (YYb1i + 1)) = (((YC . i) + 1) - (YYb1i + 1)) by A56;

          (YCe . (YYb1i + 1)) divides PP by A65, INT_4: 32;

          hence thesis by A66, A64, INT_2: 9;

        end;

        ( Product h) divides (PP - 0 ) by A30, A60, A15, INT_4: 38;

        hence (( Product (((YC . i) + 1) + ( - ( idseq x1)))), 0 ) are_congruent_mod (1 + ((Z1 + 1) * (K ! ))) by INT_1:def 4, A29;

      end;

      given Y be k -element XFinSequence of NAT , Z,K be Element of NAT such that

       A67: K > x & K >= (( sum_of_coefficients |.p.|) * ((((x ^2 ) + 1) * ( Product (1 + X))) |^ ( degree p))) and

       A68: for i be Nat st i in k holds (Y . i) > x1 and

       A69: (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

       A70: for i be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq x1)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! )));

      let z be Element of NAT such that

       A71: z <= x;

      set z1 = (z + 1), K1 = (K ! ), ZZ = (1 + ((z + 1) * K1));

      

       A72: ZZ > (1 + 0 ) by XREAL_1: 8;

      consider prim be Element of NAT such that

       A73: prim divides ZZ & prim <= ZZ & prim is prime by A72, NAT_4: 13;

      deffunc P( object) = ((Y . $1) mod prim);

      consider Yz be XFinSequence such that

       A74: ( len Yz) = k & for i be Nat st i in k holds (Yz . i) = P(i) from AFINSQ_1:sch 2;

      ( rng Yz) c= NAT

      proof

        let y be object;

        assume y in ( rng Yz);

        then

        consider x be object such that

         A75: x in ( dom Yz) & (Yz . x) = y by FUNCT_1:def 3;

        y = P(x) by A74, A75;

        hence thesis by ORDINAL1:def 12;

      end;

      then

      reconsider Yz as k -element XFinSequence of NAT by A74, RELAT_1:def 19, CARD_1:def 7;

      take Yz;

      1 <= z1 <= x1 by A71, NAT_1: 11, XREAL_1: 6;

      then

       A76: z1 in ( Seg x1);

      K >= x1 by A67, NAT_1: 13;

      then

      reconsider h = (1 + (K1 * ( idseq x1))) as CR_Sequence by Th2;

      ( rng h) c= NAT by VALUED_0:def 6;

      then

       A77: h is FinSequence of NAT by FINSEQ_1:def 4;

      

       A78: ( dom h) = ( dom (K1 * ( idseq (x + 1)))) = ( dom ( idseq (x + 1))) by VALUED_1:def 2, VALUED_1:def 5;

      

       A79: (h . z1) = (1 + ((K1 * ( idseq (x + 1))) . z1)) by A76, A78, VALUED_1:def 2

      .= (1 + (K1 * (( idseq (x + 1)) . z1))) by A76, A78, VALUED_1:def 5

      .= ZZ by A76, FINSEQ_2: 49;

      ZZ divides (1 + ((Z + 1) * K1)) by A79, A69, A77, INT_4: 32, A76, A78;

      then

       A80: prim divides (1 + ((Z + 1) * K1)) by A73, INT_2: 9;

      (1 + ((Z + 1) * K1)) divides (( eval (p,( @ (( <%Z, x%> ^ X) ^ Y)))) - 0 ) by A69, INT_1:def 4;

      then

       A81: prim divides ( eval (p,( @ (( <%Z, x%> ^ X) ^ Y)))) by A80, INT_2: 9;

      reconsider E1 = ( eval (p,( @ (( <%Z, x%> ^ X) ^ Y)))) as Integer;

      

       A82: K < prim

      proof

        assume K >= prim;

        then prim divides ((Z + 1) * K1) by INT_2: 2, A73, NEWTON: 41;

        then prim divides 1 by A80, INT_2: 1;

        then prim = 1 by INT_2: 13;

        hence thesis by A73, INT_2:def 4;

      end;

      

       A83: ( len <%z, x%>) = 2 = ( len <%Z, x%>) by CARD_1:def 7;

      

       A84: ( len ( <%z, x%> ^ X)) = (2 + n) = ( len ( <%Z, x%> ^ X)) by CARD_1:def 7;

      

       A85: ( len Y) = k = ( len Yz) by CARD_1:def 7;

      

       A86: ( len (( <%z, x%> ^ X) ^ Yz)) = ((2 + k) + n) by CARD_1:def 7;

      thus for i be Nat st i in k holds (Yz . i) <= x

      proof

        let j be Nat such that

         A87: j in k;

        set YE = (((Y . j) + 1) + ( - ( idseq x1)));

        

         A88: (Yz . j) = ((Y . j) mod prim) by A87, A74;

        

         A89: (1 + ((Z + 1) * K1)) divides (( Product YE) - 0 ) by INT_1:def 4, A70, A87;

        

         A90: ( len YE) = ( len ( idseq x1)) = x1 by CARD_1:def 7;

        

         A91: for w be Nat st w in ( dom YE) holds ((((Y . j) + 1) + ( - ( idseq x1))) . w) = (((Y . j) + 1) - w)

        proof

          let w be Nat;

          assume

           A92: w in ( dom YE);

          then w in ( dom ( - ( idseq x1))) by VALUED_1:def 2;

          then w in ( dom ( idseq x1)) by VALUED_1: 8;

          then (( idseq x1) . w) = w by FINSEQ_2: 49;

          then (( - ( idseq x1)) . w) = ( - w) by VALUED_1: 8;

          then (YE . w) = (((Y . j) + 1) + ( - w)) by A92, VALUED_1:def 2;

          hence thesis;

        end;

         A93:

        now

          let a be Nat;

          assume

           A94: a in ( dom YE);

          then 1 <= a <= x1 by A90, FINSEQ_3: 25;

          then

          reconsider a1 = (a - 1) as Nat;

          (a1 + 1) <= x1 by A94, A90, FINSEQ_3: 25;

          then a1 < x1 by NAT_1: 13;

          then

           A95: (x1 - a1) > 0 by XREAL_1: 50;

          (YE . a) = (((Y . j) + 1) - a) by A94, A91;

          then ((YE . a) + a1) > x1 by A68, A87;

          hence (YE . a) > 0 by A95, XREAL_1: 19;

        end;

        now

          let r be object;

          assume r in ( rng YE);

          then

          consider a be object such that

           A96: a in ( dom YE) & (YE . a) = r by FUNCT_1:def 3;

          reconsider a as Nat by A96;

          (YE . a) > 0 by A93, A96;

          hence r in NAT by A96, INT_1: 3;

        end;

        then

         A97: YE is FinSequence of NAT by FINSEQ_1:def 4, TARSKI:def 3;

        YE is positive-yielding

        proof

          let r be Real;

          assume r in ( rng YE);

          then

          consider a be object such that

           A98: a in ( dom YE) & (YE . a) = r by FUNCT_1:def 3;

          thus thesis by A93, A98;

        end;

        then

        consider w be Nat such that

         A99: w in ( dom YE) & prim divides (YE . w) by A89, A80, INT_2: 9, Th12, A73, A97;

        

         A100: 1 <= w <= x1 by A90, A99, FINSEQ_3: 25;

        then

        reconsider w1 = (w - 1) as Nat;

        prim divides (((Y . j) + 1) - w) by A99, A91;

        then prim divides ((Y . j) - w1);

        then (Yz . j) = (w1 mod prim) by A88, INT_4: 23, A73;

        then (Yz . j) < (w1 + 1) by NAT_1: 13, NEWTON05: 11;

        then (Yz . j) < x1 by A100, XXREAL_0: 2;

        hence thesis by NAT_1: 13;

      end;

      for i st i in ((2 + k) + n) holds prim divides (((( <%Z, x%> ^ X) ^ Y) . i) - ((( <%z, x%> ^ X) ^ Yz) . i))

      proof

        let i such that

         A101: i in ((2 + k) + n);

        per cases by A101, A86, AFINSQ_1: 20;

          suppose

           A102: i in ( dom ( <%z, x%> ^ X));

          then

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

          per cases by A102, AFINSQ_1: 20;

            suppose i in ( dom <%z, x%>);

            then

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

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

              suppose i = 0 ;

              then

               A105: ((( <%Z, x%> ^ X) ^ Y) . i) = Z & ((( <%z, x%> ^ X) ^ Yz) . i) = z by A102, A84, AFINSQ_1:def 3, A104;

              

               A106: (K1,prim) are_coprime

              proof

                assume not (K1,prim) are_coprime ;

                then

                 A107: (K1 gcd prim) <> 1 by INT_2:def 3;

                (K1 gcd prim) divides prim by INT_2:def 2;

                then (K1 gcd prim) = prim by A107, A73, INT_2:def 4;

                then prim divides K1 by INT_2:def 2;

                hence thesis by A82, NAT_4: 19, A73;

              end;

              prim divides ((1 + ((Z + 1) * K1)) - (1 + ((z + 1) * K1))) by A80, A73, INT_5: 1;

              then prim divides ((Z - z) * K1);

              hence thesis by A105, A106, INT_2: 25;

            end;

              suppose i = 1;

              hence thesis by A103, A104, INT_2: 12;

            end;

          end;

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

            then

            consider j such that

             A108: j in ( dom X) & i = (( len <%z, x%>) + j);

            (( <%z, x%> ^ X) . i) = (X . j) & (( <%Z, x%> ^ X) . i) = (X . j) by A83, A108, AFINSQ_1:def 3;

            hence thesis by INT_2: 12, A103;

          end;

        end;

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

          then

          consider j such that

           A109: j in ( dom Yz) & i = (( len ( <%z, x%> ^ X)) + j);

          

           A110: ((( <%Z, x%> ^ X) ^ Y) . i) = (Y . j) & ((( <%z, x%> ^ X) ^ Yz) . i) = (Yz . j) by A84, A85, A109, AFINSQ_1:def 3;

          (Yz . j) = ((Y . j) mod prim) by A74, A109;

          hence thesis by A110, A73, PEPIN: 8;

        end;

      end;

      then prim divides (E1 - ( eval (p,( @ (( <%z, x%> ^ X) ^ Yz))))) by A73, Th1;

      then prim divides ( eval (p,( @ (( <%z, x%> ^ X) ^ Yz)))) by INT_5: 2, A81;

      then |.prim.| divides |.( eval (p,( @ (( <%z, x%> ^ X) ^ Yz)))).| by INT_2: 16;

      then

      consider m be Nat such that

       A111: |.( eval (p,( @ (( <%z, x%> ^ X) ^ Yz)))).| = (prim * m) by NAT_D:def 3;

      

       A112: (x ^2 ) = (x * x) by SQUARE_1:def 1;

      for i be object st i in ( dom ( @ (( <%z, x%> ^ X) ^ Yz))) holds |.(( @ (( <%z, x%> ^ X) ^ Yz)) . i).| <= (((x ^2 ) + 1) * ( Product (1 + X)))

      proof

        let i be object;

        assume i in ( dom ( @ (( <%z, x%> ^ X) ^ Yz)));

        then

         A113: i in ( dom (( <%z, x%> ^ X) ^ Yz)) & (( <%z, x%> ^ X) ^ Yz) = ( @ (( <%z, x%> ^ X) ^ Yz)) by HILB10_2:def 1;

        reconsider i as Nat by A113;

        per cases by A113, AFINSQ_1: 20;

          suppose

           A114: i in ( dom ( <%z, x%> ^ X));

          then

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

          per cases by A114, AFINSQ_1: 20;

            suppose i in ( dom <%z, x%>);

            then

             A116: i in ( Segm 2) & (( <%z, x%> ^ X) . i) = ( <%z, x%> . i) by CARD_1:def 7, AFINSQ_1:def 3;

            

             A117: ( Product (1 + X)) >= 1 by NAT_1: 14;

            (x ^2 ) >= (x * 1) by NAT_1: 14, A112, XREAL_1: 64;

            then ((x ^2 ) + 1) >= (x + 0 ) by XREAL_1: 7;

            then

             A118: (((x ^2 ) + 1) * ( Product (1 + X))) >= (x * 1) by A117, XREAL_1: 66;

            i = 0 or i = 1 by A116, NAT_1: 23, NAT_1: 44;

            hence thesis by A118, A71, XXREAL_0: 2, A115, A116;

          end;

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

            then

            consider j such that

             A119: j in ( dom X) & i = (( len <%z, x%>) + j);

            

             A120: ( dom (1 + X)) = ( dom X) by VALUED_1:def 2;

            then

             A121: ((1 + X) . j) <= ( Product (1 + X)) by A119, HILB10_4: 11;

            ((1 + X) . j) = (1 + (X . j)) by A119, A120, VALUED_1:def 2;

            then

             A122: (X . j) <= ( Product (1 + X)) by A121, NAT_1: 13;

            ((x ^2 ) + 1) >= 1 by NAT_1: 11;

            then (1 * (X . j)) <= (((x ^2 ) + 1) * ( Product (1 + X))) by A122, XREAL_1: 66;

            hence thesis by A119, AFINSQ_1:def 3, A115;

          end;

        end;

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

          then

          consider j such that

           A123: j in ( dom Yz) & i = (( len ( <%z, x%> ^ X)) + j);

          set YE = (((Y . j) + 1) + ( - ( idseq x1)));

          

           A124: ((( <%z, x%> ^ X) ^ Yz) . i) = (Yz . j) by A123, AFINSQ_1:def 3;

          

           A125: (Yz . j) = ((Y . j) mod prim) by A123, A74;

          

           A126: (1 + ((Z + 1) * K1)) divides (( Product YE) - 0 ) by INT_1:def 4, A70, A123, A74;

          

           A127: ( len YE) = ( len ( idseq x1)) = x1 by CARD_1:def 7;

          

           A128: for w be Nat st w in ( dom YE) holds ((((Y . j) + 1) + ( - ( idseq x1))) . w) = (((Y . j) + 1) - w)

          proof

            let w be Nat;

            assume

             A129: w in ( dom YE);

            then w in ( dom ( - ( idseq x1))) by VALUED_1:def 2;

            then w in ( dom ( idseq x1)) by VALUED_1: 8;

            then (( idseq x1) . w) = w by FINSEQ_2: 49;

            then (( - ( idseq x1)) . w) = ( - w) by VALUED_1: 8;

            then (YE . w) = (((Y . j) + 1) + ( - w)) by A129, VALUED_1:def 2;

            hence thesis;

          end;

           A130:

          now

            let a be Nat;

            assume

             A131: a in ( dom YE);

            1 <= a <= x1 by A131, A127, FINSEQ_3: 25;

            then

            reconsider a1 = (a - 1) as Nat;

            (a1 + 1) <= x1 by A131, A127, FINSEQ_3: 25;

            then a1 < x1 by NAT_1: 13;

            then

             A132: (x1 - a1) > 0 by XREAL_1: 50;

            (YE . a) = (((Y . j) + 1) - a) by A131, A128;

            then ((YE . a) + a1) > x1 by A68, A85, A123;

            hence (YE . a) > 0 by A132, XREAL_1: 19;

          end;

          now

            let r be object;

            assume r in ( rng YE);

            then

            consider a be object such that

             A133: a in ( dom YE) & (YE . a) = r by FUNCT_1:def 3;

            reconsider a as Nat by A133;

            (YE . a) > 0 by A130, A133;

            hence r in NAT by A133, INT_1: 3;

          end;

          then

           A134: YE is FinSequence of NAT by FINSEQ_1:def 4, TARSKI:def 3;

          YE is positive-yielding

          proof

            let r be Real;

            assume r in ( rng YE);

            then

            consider a be object such that

             A135: a in ( dom YE) & (YE . a) = r by FUNCT_1:def 3;

            thus thesis by A130, A135;

          end;

          then

          consider w be Nat such that

           A136: w in ( dom YE) & prim divides (YE . w) by A126, A80, INT_2: 9, Th12, A73, A134;

          

           A137: 1 <= w <= x1 by A127, A136, FINSEQ_3: 25;

          then

          reconsider w1 = (w - 1) as Nat;

          prim divides (((Y . j) + 1) - w) by A136, A128;

          then prim divides ((Y . j) - w1);

          then (Yz . j) = (w1 mod prim) by A125, INT_4: 23, A73;

          then (Yz . j) < (w1 + 1) by NAT_1: 13, NEWTON05: 11;

          then

           A138: (Yz . j) < x1 by A137, XXREAL_0: 2;

          (x ^2 ) >= (x * 1) by NAT_1: 14, A112, XREAL_1: 64;

          then ((x ^2 ) + 1) >= x1 by XREAL_1: 7;

          then

           A139: (Yz . j) < ((x ^2 ) + 1) by A138, XXREAL_0: 2;

          ( Product (1 + X)) >= 1 by NAT_1: 14;

          then (1 * (Yz . j)) <= (((x ^2 ) + 1) * ( Product (1 + X))) by A139, XREAL_1: 66;

          hence thesis by A124, A113;

        end;

      end;

      then |.( eval (p,( @ (( <%z, x%> ^ X) ^ Yz)))).| <= (( sum_of_coefficients |.p.|) * ((((x ^2 ) + 1) * ( Product (1 + X))) |^ ( degree p))) by NAT_1: 14, Th10;

      then |.( eval (p,( @ (( <%z, x%> ^ X) ^ Yz)))).| <= K by A67, XXREAL_0: 2;

      then (prim * m) < (prim * 1) by A111, A82, XXREAL_0: 2;

      then m < 1 by XREAL_1: 66;

      then m = 0 by NAT_1: 14;

      hence thesis by A111;

    end;

    theorem :: HILB10_5:18

    for p be INT -valued Polynomial of ((2 + n) + k), F_Real holds { X where X be n -element XFinSequence of NAT : ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let p be INT -valued Polynomial of ((2 + n) + k), F_Real ;

      set X0 = { X where X be n -element XFinSequence of NAT : ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 };

      set NK = ((1 + n) + k), sum = ( sum_of_coefficients |.p.|), Deg = ( degree p);

      

       A1: 0 < (NK + 4) & (NK + 0 ) < (NK + 4) & (NK + 1) < (NK + 4) & (NK + 2) < (NK + 4) & (NK + 3) < (NK + 4) by XREAL_1: 8;

      then 0 in ( Segm (NK + 4)) & (NK + 0 ) in ( Segm (NK + 4)) & (NK + 1) in ( Segm (NK + 4)) & (NK + 2) in ( Segm (NK + 4)) & (NK + 3) in ( Segm (NK + 4)) by NAT_1: 44;

      then

      reconsider ZERO = 0 , i0 = NK, i1 = (NK + 1), i2 = (NK + 2), i3 = (NK + 3) as Element of (NK + 4);

      defpred P2[ XFinSequence of NAT ] means (1 * ($1 . i1)) > ((1 * ($1 . ZERO)) + 0 );

      

       A2: { q where q be (NK + 4) -element XFinSequence of NAT : P2[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_3: 7;

      defpred P3[ XFinSequence of NAT ] means ($1 . i1) >= (sum * (((((($1 . ZERO) ^2 ) + 1) * ( Product (1 + (($1 /^ 1) | n)))) * ((1 * ($1 . i0)) + 0 )) |^ (( 0 * ($1 . i0)) + Deg)));

      (1 + n) <= NK by NAT_1: 11;

      then

       A3: { q where q be (NK + 4) -element XFinSequence of NAT : P3[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by Th11, A1, XXREAL_0: 2;

      defpred P4[ XFinSequence of NAT ] means for i be Nat st i in k holds ($1 . ((1 + n) + i)) > ($1 . i0) & (( Product ((($1 . ((1 + n) + i)) + 1) + ( - ( idseq ($1 . i0))))), 0 ) are_congruent_mod ($1 . i2);

      

       A4: { q where q be (NK + 4) -element XFinSequence of NAT : P4[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT )

      proof

        defpred T[ Nat, Nat, Nat, Nat] means (( Product (($1 + 1) + ( - ( idseq $2)))), 0 ) are_congruent_mod $3 & $1 > $2;

        

         A5: for i1,i2,i3,i4 be Element of (NK + 4) holds { q where q be (NK + 4) -element XFinSequence of NAT : T[(q . i1), (q . i2), (q . i3), (q . i4)] } is diophantine Subset of ((NK + 4) -xtuples_of NAT )

        proof

          let i1,i2,i3,i4 be Element of (NK + 4);

          set NK5 = ((NK + 4) + 1);

          

           A6: ((NK + 4) + 0 ) < NK5 by NAT_1: 13;

          then (NK + 4) in ( Segm NK5) by NAT_1: 44;

          then

          reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, M0 = (NK + 4) as Element of NK5 by HILB10_3: 2;

          defpred G[ XFinSequence of NAT ] means ($1 . M0) = ( Product ((($1 . I1) + 1) + ( - ( idseq ($1 . I2))))) & ($1 . I1) > ($1 . I2);

          

           A7: { q where q be NK5 -element XFinSequence of NAT : G[q] } is diophantine Subset of (NK5 -xtuples_of NAT ) by HILB10_4: 38;

          defpred H[ XFinSequence of NAT ] means ((1 * ($1 . M0)),( 0 * ($1 . I4))) are_congruent_mod (1 * ($1 . I3));

          

           A8: { q where q be NK5 -element XFinSequence of NAT : H[q] } is diophantine Subset of (NK5 -xtuples_of NAT ) by HILB10_3: 21;

          set GH = { q where q be NK5 -element XFinSequence of NAT : G[q] & H[q] };

          set GHr = { (q | (NK + 4)) where q be NK5 -element XFinSequence of NAT : q in GH };

          set QQ = { q where q be (NK + 4) -element XFinSequence of NAT : T[(q . i1), (q . i2), (q . i3), (q . i4)] };

          

           A9: GH is diophantine Subset of (NK5 -xtuples_of NAT ) from HILB10_3:sch 3( A7, A8);

          

           A10: GHr is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by A9, NAT_1: 11, HILB10_3: 5;

          

           A11: GHr c= QQ

          proof

            let y be object such that

             A12: y in GHr;

            consider q be NK5 -element XFinSequence of NAT such that

             A13: y = (q | (NK + 4)) & q in GH by A12;

            

             A14: ex w be NK5 -element XFinSequence of NAT st w = q & G[w] & H[w] by A13;

            ( len q) = NK5 by CARD_1:def 7;

            then ( len (q | (NK + 4))) = (NK + 4) by A6, AFINSQ_1: 54;

            then

            reconsider Q = (q | (NK + 4)) as (NK + 4) -element XFinSequence of NAT by CARD_1:def 7;

            (Q . i1) = (q . I1) & (Q . i2) = (q . I2) & (Q . i3) = (q . I3) & (Q . i4) = (q . I4) by HILB10_3: 4;

            hence thesis by A14, A13;

          end;

          QQ c= GHr

          proof

            let y be object;

            assume y in QQ;

            then

            consider q be (NK + 4) -element XFinSequence of NAT such that

             A15: y = q & T[(q . i1), (q . i2), (q . i3), (q . i4)];

            ( Product (((q . i1) + 1) + ( - ( idseq (q . i2))))) = (((q . i2) ! ) * ((q . i1) choose (q . i2))) by HILB10_4: 23, A15;

            then

            reconsider P = ( Product (((q . i1) + 1) + ( - ( idseq (q . i2))))) as Element of NAT ;

            set qP = (q ^ <%P%>);

            

             A16: ( len q) = (NK + 4) by CARD_1:def 7;

            

             A17: (qP | (NK + 4)) = q by A16, AFINSQ_1: 57;

            (qP . i1) = (q . i1) & (qP . i2) = (q . i2) & (qP . i3) = (q . i3) by A17, HILB10_3: 4;

            then G[qP] & H[qP] by A16, AFINSQ_1: 36, A15;

            then qP in GH;

            hence thesis by A15, A17;

          end;

          hence thesis by A10, A11, XBOOLE_0:def 10;

        end;

        set SN = { ((1 + n) + i) where i be Nat : i in k };

        

         A18: SN c= ( Segm (NK + 4))

        proof

          let x be object;

          assume x in SN;

          then

          consider i be Nat such that

           A19: x = ((1 + n) + i) & i in k;

          i in ( Segm k) by A19;

          then (i + 0 ) < (k + 4) by NAT_1: 44, XREAL_1: 8;

          then ((1 + n) + (i + 0 )) < ((1 + n) + (k + 4)) by XREAL_1: 8;

          hence thesis by A19, NAT_1: 44;

        end;

        set PP = { p where p be (NK + 4) -element XFinSequence of NAT : for i be Nat st i in SN holds T[(p . i), (p . i0), (p . i2), (p . i2)] };

        for i2,i3,i4 be Element of (NK + 4) holds { p where p be (NK + 4) -element XFinSequence of NAT : for i be Nat st i in SN holds T[(p . i), (p . i2), (p . i3), (p . i4)] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from SubsetDioph( A5, A18);

        then

         A20: PP is diophantine Subset of ((NK + 4) -xtuples_of NAT );

        set QQ = { q where q be (NK + 4) -element XFinSequence of NAT : P4[q] };

        

         A21: QQ c= PP

        proof

          let x be object;

          assume x in QQ;

          then

          consider p be (NK + 4) -element XFinSequence of NAT such that

           A22: x = p & P4[p];

          for i be Nat st i in SN holds T[(p . i), (p . i0), (p . i2), (p . i2)]

          proof

            let i be Nat;

            assume i in SN;

            then ex j be Nat st i = ((1 + n) + j) & j in k;

            hence T[(p . i), (p . i0), (p . i2), (p . i2)] by A22;

          end;

          hence thesis by A22;

        end;

        PP c= QQ

        proof

          let x be object;

          assume x in PP;

          then

          consider p be (NK + 4) -element XFinSequence of NAT such that

           A23: x = p & for i be Nat st i in SN holds T[(p . i), (p . i0), (p . i2), (p . i2)];

           P4[p]

          proof

            let i such that

             A24: i in k;

            ((1 + n) + i) in SN by A24;

            hence thesis by A23;

          end;

          hence thesis by A23;

        end;

        hence thesis by A20, XBOOLE_0:def 10, A21;

      end;

      defpred P5[ XFinSequence of NAT ] means (1 * ($1 . i0)) > ((1 * ($1 . ZERO)) + 0 );

      

       A25: { q where q be (NK + 4) -element XFinSequence of NAT : P5[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_3: 7;

      defpred P6[ XFinSequence of NAT ] means (1 + ((($1 . i3) + 1) * (($1 . i1) ! ))) = ($1 . i2);

      

       A26: { q where q be (NK + 4) -element XFinSequence of NAT : P6[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_4: 33;

      defpred P7[ XFinSequence of NAT ] means ($1 . i2) = ( Product (1 + ((($1 . i1) ! ) * ( idseq (1 + ($1 . ZERO))))));

      

       A27: { q where q be (NK + 4) -element XFinSequence of NAT : P7[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_4: 36;

      reconsider R = p as INT -valued Polynomial of (1 + NK), F_Real ;

      defpred P8[ XFinSequence of NAT ] means for Y be (1 + NK) -element XFinSequence of NAT st Y = ( <%($1 . i3)%> ^ ($1 | NK)) holds (( eval (R,( @ Y))), 0 ) are_congruent_mod ($1 . i2);

      (NK + 0 ) < (NK + 3) by XREAL_1: 8;

      then (NK + 1) <= (NK + 4) & NK in ( Segm i3) by XREAL_1: 8, NAT_1: 44;

      then

       A28: { q where q be (NK + 4) -element XFinSequence of NAT : P8[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by Th15;

      defpred P123[ XFinSequence of NAT ] means P2[$1] & P3[$1];

      

       A29: { q where q be (NK + 4) -element XFinSequence of NAT : P123[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A2, A3);

      defpred P1234[ XFinSequence of NAT ] means P123[$1] & P4[$1];

      

       A30: { q where q be (NK + 4) -element XFinSequence of NAT : P1234[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A29, A4);

      defpred P12345[ XFinSequence of NAT ] means P1234[$1] & P5[$1];

      

       A31: { q where q be (NK + 4) -element XFinSequence of NAT : P12345[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A30, A25);

      defpred P123456[ XFinSequence of NAT ] means P12345[$1] & P6[$1];

      

       A32: { q where q be (NK + 4) -element XFinSequence of NAT : P123456[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A31, A26);

      defpred P1234567[ XFinSequence of NAT ] means P123456[$1] & P7[$1];

      

       A33: { q where q be (NK + 4) -element XFinSequence of NAT : P1234567[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A32, A27);

      defpred P12345678[ XFinSequence of NAT ] means P1234567[$1] & P8[$1];

      set X3 = { q where q be (NK + 4) -element XFinSequence of NAT : P12345678[q] };

      

       A34: X3 is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A33, A28);

      set X2 = { (X | (n + 1)) where X be (NK + 4) -element XFinSequence of NAT : X in X3 };

      (n + 1) <= ((1 + n) + (k + 4)) by NAT_1: 11;

      then

       A35: X2 is diophantine Subset of ((n + 1) -xtuples_of NAT ) by A34, HILB10_3: 5;

      defpred S[ XFinSequence of NAT ] means for z be Element of NAT st z <= ($1 . 0 ) holds ex y be k -element XFinSequence of NAT st for X1 be n -element XFinSequence of NAT st X1 = ($1 /^ 1) holds ( eval (p,( @ (( <%z, ($1 . 0 )%> ^ X1) ^ y)))) = 0 ;

      set X1 = { X where X be (n + 1) -element XFinSequence of NAT : S[X] };

      for s be object holds s in X1 iff s in X2

      proof

        let s be object;

        thus s in X1 implies s in X2

        proof

          assume s in X1;

          then

          consider h be (n + 1) -element XFinSequence of NAT such that

           A36: s = h & S[h];

          set X = (h /^ 1);

          ( len h) = (n + 1) >= 1 by NAT_1: 11, CARD_1:def 7;

          then

           A37: ( len X) = ((n + 1) -' 1) by AFINSQ_2:def 2;

          then

           A38: ( len X) = n by NAT_D: 34;

          reconsider X as n -element XFinSequence of NAT by A37, NAT_D: 34, CARD_1:def 7;

          set x = (h . 0 );

          for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0

          proof

            let z be Element of NAT such that

             A39: z <= x;

            consider y be k -element XFinSequence of NAT such that

             A40: for X1 be n -element XFinSequence of NAT st X1 = (h /^ 1) holds ( eval (p,( @ (( <%z, x%> ^ X1) ^ y)))) = 0 by A39, A36;

            ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 by A40;

            hence thesis;

          end;

          then

          consider Y be k -element XFinSequence of NAT , Z,e,K be Element of NAT such that

           A41: K > x & K >= (sum * (((((x ^2 ) + 1) * ( Product (1 + X))) * e) |^ Deg)) and

           A42: for i be Nat st i in k holds (Y . i) > e and

           A43: e > x and

           A44: (1 + ((Z + 1) * (K ! ))) = ( Product (1 + ((K ! ) * ( idseq (x + 1))))) and

           A45: (( eval (p,( @ (( <%Z, x%> ^ X) ^ Y)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))) and

           A46: for i be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq e)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))) by Th16;

          set xXY = (( <%x%> ^ X) ^ Y), E = ((( <%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K ! )))%>) ^ <%Z%>);

          set H = (xXY ^ E);

           0 in ( Segm 1) by NAT_1: 44;

          then

           A47: 0 in ( dom <%x%>) & ( len <%x%>) = 1 & ( dom <%x%>) c= ( dom ( <%x%> ^ X)) by AFINSQ_1: 21, AFINSQ_1: 33;

          then 0 in ( dom ( <%x%> ^ X)) & ( dom ( <%x%> ^ X)) c= ( dom xXY) by AFINSQ_1: 21;

          

          then

           A48: (H . 0 ) = (xXY . 0 ) by AFINSQ_1:def 3

          .= (( <%x%> ^ X) . 0 ) by AFINSQ_1:def 3, A47

          .= ( <%x%> . 0 ) by AFINSQ_1:def 3, A47;

          H = (( <%x%> ^ (X ^ Y)) ^ E) by AFINSQ_1: 27

          .= ( <%x%> ^ ((X ^ Y) ^ E)) by AFINSQ_1: 27;

          

          then

           A49: (H /^ 1) = ((X ^ Y) ^ E) by A47, AFINSQ_2: 12

          .= (X ^ (Y ^ E)) by AFINSQ_1: 27;

          

           A50: ( len xXY) = NK by CARD_1:def 7;

          then

           A51: (H | NK) = xXY by AFINSQ_1: 57;

          

           A52: ( len E) = 4 by CARD_1:def 7;

           0 in ( dom E) by AFINSQ_1: 66;

          

          then

           A53: (H . (NK + 0 )) = (E . 0 ) by A50, AFINSQ_1:def 3

          .= e by AFINSQ_1: 45;

          1 in ( dom E) by A52, AFINSQ_1: 66;

          

          then

           A54: (H . (NK + 1)) = (E . 1) by A50, AFINSQ_1:def 3

          .= K by AFINSQ_1: 45;

          2 in ( dom E) by A52, AFINSQ_1: 66;

          

          then

           A55: (H . (NK + 2)) = (E . 2) by A50, AFINSQ_1:def 3

          .= (1 + ((Z + 1) * (K ! ))) by AFINSQ_1: 45;

          3 in ( dom E) by A52, AFINSQ_1: 66;

          

          then

           A56: (H . (NK + 3)) = (E . 3) by A50, AFINSQ_1:def 3

          .= Z by AFINSQ_1: 45;

          

           A57: for i be Nat st i in k holds (H . ((1 + n) + i)) = (Y . i)

          proof

            let i be Nat such that

             A58: i in k;

            

             A59: ( len Y) = k & ( len ( <%x%> ^ X)) = (1 + n) by CARD_1:def 7;

            then ((1 + n) + i) in ( dom xXY) by AFINSQ_1: 23, A58;

            

            hence (H . ((1 + n) + i)) = (xXY . ((1 + n) + i)) by AFINSQ_1:def 3

            .= (Y . i) by A59, A58, AFINSQ_1:def 3;

          end;

          

           A60: for i be Nat st i in k holds (H . ((1 + n) + i)) > (H . NK)

          proof

            let i be Nat such that

             A61: i in k;

            (H . ((1 + n) + i)) = (Y . i) by A61, A57;

            hence thesis by A53, A42, A61;

          end;

          

           A62: for Y be ((2 + n) + k) -element XFinSequence of NAT st Y = ( <%(H . (NK + 3))%> ^ (H | NK)) holds (( eval (p,( @ Y))), 0 ) are_congruent_mod (H . (NK + 2))

          proof

            let YY be ((2 + n) + k) -element XFinSequence of NAT such that

             A63: YY = ( <%(H . (NK + 3))%> ^ (H | NK));

            YY = ( <%Z%> ^ ( <%x%> ^ (X ^ Y))) by A56, AFINSQ_1: 27, A51, A63

            .= (( <%Z%> ^ <%x%>) ^ (X ^ Y)) by AFINSQ_1: 27

            .= (( <%Z, x%> ^ X) ^ Y) by AFINSQ_1: 27;

            hence thesis by A45, A55;

          end;

          

           A64: for i be Nat st i in k holds (( Product (((H . ((1 + n) + i)) + 1) + ( - ( idseq (H . NK))))), 0 ) are_congruent_mod (H . (NK + 2))

          proof

            let i be Nat such that

             A65: i in k;

            (H . ((1 + n) + i)) = (Y . i) by A65, A57;

            hence thesis by A53, A55, A46, A65;

          end;

          

           A66: P2[H] by A48, A54, A41;

          

           A67: P3[H] by A48, A49, A38, AFINSQ_1: 57, A53, A54, A41;

          

           A68: P4[H] by A60, A64;

          H in X3 by A66, A67, A68, A53, A43, A56, A48, A54, A55, A44, A62;

          then

           A69: (H | (n + 1)) in X2;

          (H | (n + 1)) = (xXY | (n + 1)) & ( len ( <%x%> ^ X)) = (1 + n) by NAT_1: 11, A50, AFINSQ_1: 58, CARD_1:def 7;

          then (H | (n + 1)) = ( <%x%> ^ X) by AFINSQ_1: 57;

          hence thesis by A36, A69, NUMERAL2: 2;

        end;

        assume s in X2;

        then

        consider x be (NK + 4) -element XFinSequence of NAT such that

         A70: s = (x | (n + 1)) & x in X3;

        consider H be (NK + 4) -element XFinSequence of NAT such that

         A71: H = x and

         A72: P12345678[H] by A70;

        

         A73: (NK + 4) >= NK & ( len H) = (NK + 4) by NAT_1: 11, CARD_1:def 7;

        then

         A74: ( len (H | NK)) = NK by AFINSQ_1: 54;

        then

         A75: ( len ((H | NK) /^ (n + 1))) = (NK -' (n + 1)) by AFINSQ_2:def 2;

        then

         A76: ( len ((H | NK) /^ (n + 1))) = k by NAT_D: 34;

        reconsider Y = ((H | NK) /^ (n + 1)) as k -element XFinSequence of NAT by A75, NAT_D: 34, CARD_1:def 7;

        reconsider x = (H . 0 ), e = (H . NK), K = (H . (NK + 1)), Z = (H . (NK + 3)) as Element of NAT ;

        

         A77: ( len H) = ((NK + 3) + 1) by CARD_1:def 7;

        then ( len (H /^ 1)) = (((NK + 3) + 1) -' 1) by AFINSQ_2:def 2;

        then

         A78: ( len (H /^ 1)) = (NK + 3) by NAT_D: 34;

        (((1 + k) + 3) + n) >= n by NAT_1: 11;

        then ( len ((H /^ 1) | n)) = n by AFINSQ_1: 54, A78;

        then

        reconsider X = ((H /^ 1) | n) as n -element XFinSequence of NAT by CARD_1:def 7;

        

         A79: for i be Nat st i in k holds (Y . i) = (H . ((1 + n) + i))

        proof

          let i be Nat such that

           A80: i in k;

          

           A81: (Y . i) = ((H | NK) . ((n + 1) + i)) by A80, A76, AFINSQ_2:def 2;

          i in ( Segm k) by A80;

          then ((1 + n) + i) < ( Segm NK) by XREAL_1: 8, NAT_1: 44;

          hence thesis by A81, NAT_1: 44, FUNCT_1: 49;

        end;

        

         A82: for i be Nat st i in k holds (Y . i) > e

        proof

          let i such that

           A83: i in k;

          (Y . i) = (H . ((1 + n) + i)) by A83, A79;

          hence thesis by A83, A72;

        end;

        ( len <%Z%>) = 1 by CARD_1:def 7;

        then ( len ( <%Z%> ^ (H | NK))) = (1 + NK) by A74, AFINSQ_1: 17;

        then

        reconsider ZY = ( <%Z%> ^ (H | NK)) as ((2 + n) + k) -element XFinSequence of NAT by CARD_1:def 7;

        ( Segm (n + 1)) c= ( Segm NK) by NAT_1: 11, NAT_1: 39;

        then ((H | NK) | (n + 1)) = (H | (n + 1)) by RELAT_1: 74;

        then

         A84: (H | NK) = ((H | (n + 1)) ^ Y);

        

         A85: ((1 + 1) -' 1) = 1 & ((n + 2) -' 2) = n by NAT_D: 34;

        (n + 1) <= ((n + 1) + (k + 4)) by NAT_1: 11;

        

        then

         A86: ((H /^ ((1 + 1) -' 1)) | (((n + 1) + 1) -' (1 + 1))) = ( mid (H,(1 + 1),(n + 1))) by A73, AFINSQ_2: 15

        .= ((H | (n + 1)) /^ ((1 + 1) -' 1)) by AFINSQ_2:def 3;

        

         A87: (H | (n + 1)) = (((H | (n + 1)) | 1) ^ ((H /^ 1) | n)) by A85, A86;

        ( Segm 1) c= ( Segm (n + 1)) by NAT_1: 11, NAT_1: 39;

        

        then ((H | (n + 1)) | 1) = (H | 1) by RELAT_1: 74

        .= <%(H . 0 )%> by NUMERAL2: 1;

        

        then ZY = ( <%Z%> ^ ( <%x%> ^ (X ^ Y))) by A84, A87, AFINSQ_1: 27

        .= (( <%Z%> ^ <%x%>) ^ (X ^ Y)) by AFINSQ_1: 27

        .= (( <%Z, x%> ^ X) ^ Y) by AFINSQ_1: 27;

        then

         A88: (( eval (p,( @ (( <%Z, x%> ^ X) ^ Y)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))) by A72;

        

         A89: for i be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq e)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! )))

        proof

          let i;

          assume

           A90: i in k;

          then (Y . i) = (H . ((n + 1) + i)) by A79;

          hence thesis by A90, A72;

        end;

        (n + 1) <= ((n + 1) + (k + 4)) by NAT_1: 11;

        then ( len (H | (n + 1))) = (n + 1) by AFINSQ_1: 54, A77;

        then

        reconsider F = (H | (n + 1)) as (n + 1) -element XFinSequence of NAT by CARD_1:def 7;

        

         A91: 0 < ( len F);

        then

         A92: (F . 0 ) = (H . 0 ) by FUNCT_1: 47, AFINSQ_1: 66;

        for z be Element of NAT st z <= (F . 0 ) holds ex y be k -element XFinSequence of NAT st for X1 be n -element XFinSequence of NAT st X1 = (F /^ 1) holds ( eval (p,( @ (( <%z, (F . 0 )%> ^ X1) ^ y)))) = 0

        proof

          let z be Element of NAT such that

           A93: z <= (F . 0 );

          consider y be k -element XFinSequence of NAT such that

           A94: ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 by A93, A92, A89, Th16, A72, A82, A88;

          take y;

          let X1 be n -element XFinSequence of NAT ;

          assume X1 = (F /^ 1);

          hence thesis by A94, A91, FUNCT_1: 47, AFINSQ_1: 66, A86, A85;

        end;

        hence thesis by A71, A70;

      end;

      then

       A95: X1 = X2 by TARSKI: 2;

      set Y1 = { (X /^ 1) where X be (n + 1) -element XFinSequence of NAT : X in X1 };

      

       A96: Y1 is diophantine Subset of (n -xtuples_of NAT ) by A95, A35, HILB10_4: 27;

      for s be object holds s in Y1 iff s in X0

      proof

        let s be object;

        thus s in Y1 implies s in X0

        proof

          assume s in Y1;

          then

          consider xS be (n + 1) -element XFinSequence of NAT such that

           A97: s = (xS /^ 1) & xS in X1;

          

           A98: ex w be (n + 1) -element XFinSequence of NAT st xS = w & S[w] by A97;

          ( len xS) = (n + 1) by CARD_1:def 7;

          then ( len (xS /^ 1)) = ((n + 1) -' 1) by AFINSQ_2:def 2;

          then

          reconsider S = (xS /^ 1) as n -element XFinSequence of NAT by NAT_D: 34, CARD_1:def 7;

          ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0

          proof

            take x = (xS . 0 );

            let z be Element of NAT such that

             A99: z <= x;

            consider y be k -element XFinSequence of NAT such that

             A100: for X1 be n -element XFinSequence of NAT st X1 = (xS /^ 1) holds ( eval (p,( @ (( <%z, (xS . 0 )%> ^ X1) ^ y)))) = 0 by A98, A99;

            ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0 by A100;

            hence thesis;

          end;

          hence thesis by A97;

        end;

        assume s in X0;

        then

        consider S be n -element XFinSequence of NAT such that

         A101: s = S & ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0 ;

        consider x be Element of NAT such that

         A102: for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0 by A101;

        set xS = ( <%x%> ^ S);

        

         A103: ( len <%x%>) = 1 by CARD_1:def 7;

        then

         A104: (xS /^ 1) = S by AFINSQ_2: 12;

         S[xS]

        proof

          let z be Element of NAT such that

           A105: z <= (xS . 0 );

          

           A106: (xS . 0 ) = x by AFINSQ_1: 35;

          then

          consider y be k -element XFinSequence of NAT such that

           A107: ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0 by A102, A105;

          take y;

          thus thesis by AFINSQ_2: 12, A103, A106, A107;

        end;

        then xS in X1;

        hence s in Y1 by A104, A101;

      end;

      hence thesis by A96, TARSKI: 2;

    end;

    theorem :: HILB10_5:19

    

     Th19: for p be INT -valued Polynomial of ((2 + n) + k), F_Real holds { X where X be n -element XFinSequence of NAT : ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i be Nat st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 } is diophantine Subset of (n -xtuples_of NAT )

    proof

      let p be INT -valued Polynomial of ((2 + n) + k), F_Real ;

      set X0 = { X where X be n -element XFinSequence of NAT : ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i be Nat st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 };

      set NK = ((1 + n) + k), sum = ( sum_of_coefficients |.p.|), Deg = ( degree p);

      

       A1: 0 < (NK + 4) & (NK + 0 ) < (NK + 4) & (NK + 1) < (NK + 4) & (NK + 2) < (NK + 4) & (NK + 2) < (NK + 4) by XREAL_1: 8;

      then 0 in ( Segm (NK + 4)) & (NK + 0 ) in ( Segm (NK + 4)) & (NK + 1) in ( Segm (NK + 4)) & (NK + 2) in ( Segm (NK + 4)) by NAT_1: 44;

      then

      reconsider ZERO = 0 , i0 = NK, i1 = (NK + 1), i2 = (NK + 2), i3 = (NK + 3) as Element of (NK + 4) by HILB10_3: 3;

      defpred P2[ XFinSequence of NAT ] means (1 * ($1 . i1)) > ((1 * ($1 . ZERO)) + 0 );

      

       A2: { q where q be (NK + 4) -element XFinSequence of NAT : P2[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_3: 7;

      defpred P3[ XFinSequence of NAT ] means ($1 . i1) >= (sum * (((((($1 . ZERO) ^2 ) + 1) * ( Product (1 + (($1 /^ 1) | n)))) * (( 0 * ($1 . i0)) + 1)) |^ (( 0 * ($1 . i0)) + Deg)));

      (1 + n) <= NK by NAT_1: 11;

      then

       A3: { q where q be (NK + 4) -element XFinSequence of NAT : P3[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by Th11, A1, XXREAL_0: 2;

      defpred P4[ XFinSequence of NAT ] means for i be Nat st i in k holds ($1 . ((1 + n) + i)) > ($1 . i0) & (( Product ((($1 . ((1 + n) + i)) + 1) + ( - ( idseq ($1 . i0))))), 0 ) are_congruent_mod ($1 . i2);

      

       A4: { q where q be (NK + 4) -element XFinSequence of NAT : P4[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT )

      proof

        defpred T[ Nat, Nat, Nat, Nat] means (( Product (($1 + 1) + ( - ( idseq $2)))), 0 ) are_congruent_mod $3 & $1 > $2;

        

         A5: for i1,i2,i3,i4 be Element of (NK + 4) holds { q where q be (NK + 4) -element XFinSequence of NAT : T[(q . i1), (q . i2), (q . i3), (q . i4)] } is diophantine Subset of ((NK + 4) -xtuples_of NAT )

        proof

          let i1,i2,i3,i4 be Element of (NK + 4);

          set NK5 = ((NK + 4) + 1);

          

           A6: ((NK + 4) + 0 ) < NK5 by NAT_1: 13;

          then (NK + 4) in ( Segm NK5) by NAT_1: 44;

          then

          reconsider I1 = i1, I2 = i2, I3 = i3, I4 = i4, M0 = (NK + 4) as Element of NK5 by HILB10_3: 2;

          defpred G[ XFinSequence of NAT ] means ($1 . M0) = ( Product ((($1 . I1) + 1) + ( - ( idseq ($1 . I2))))) & ($1 . I1) > ($1 . I2);

          

           A7: { q where q be NK5 -element XFinSequence of NAT : G[q] } is diophantine Subset of (NK5 -xtuples_of NAT ) by HILB10_4: 38;

          defpred H[ XFinSequence of NAT ] means ((1 * ($1 . M0)),( 0 * ($1 . I4))) are_congruent_mod (1 * ($1 . I3));

          

           A8: { q where q be NK5 -element XFinSequence of NAT : H[q] } is diophantine Subset of (NK5 -xtuples_of NAT ) by HILB10_3: 21;

          set GH = { q where q be NK5 -element XFinSequence of NAT : G[q] & H[q] };

          set GHr = { (q | (NK + 4)) where q be NK5 -element XFinSequence of NAT : q in GH };

          set QQ = { q where q be (NK + 4) -element XFinSequence of NAT : T[(q . i1), (q . i2), (q . i3), (q . i4)] };

          

           A9: GH is diophantine Subset of (NK5 -xtuples_of NAT ) from HILB10_3:sch 3( A7, A8);

          

           A10: GHr is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by A9, HILB10_3: 5, NAT_1: 11;

          

           A11: GHr c= QQ

          proof

            let y be object such that

             A12: y in GHr;

            consider q be NK5 -element XFinSequence of NAT such that

             A13: y = (q | (NK + 4)) & q in GH by A12;

            

             A14: ex w be NK5 -element XFinSequence of NAT st w = q & G[w] & H[w] by A13;

            ( len q) = NK5 by CARD_1:def 7;

            then ( len (q | (NK + 4))) = (NK + 4) by A6, AFINSQ_1: 54;

            then

            reconsider Q = (q | (NK + 4)) as (NK + 4) -element XFinSequence of NAT by CARD_1:def 7;

            (Q . i1) = (q . I1) & (Q . i2) = (q . I2) & (Q . i3) = (q . I3) & (Q . i4) = (q . I4) by HILB10_3: 4;

            hence thesis by A13, A14;

          end;

          QQ c= GHr

          proof

            let y be object;

            assume y in QQ;

            then

            consider q be (NK + 4) -element XFinSequence of NAT such that

             A15: y = q & T[(q . i1), (q . i2), (q . i3), (q . i4)];

            ( Product (((q . i1) + 1) + ( - ( idseq (q . i2))))) = (((q . i2) ! ) * ((q . i1) choose (q . i2))) by A15, HILB10_4: 23;

            then

            reconsider P = ( Product (((q . i1) + 1) + ( - ( idseq (q . i2))))) as Element of NAT ;

            set qP = (q ^ <%P%>);

            

             A16: ( len q) = (NK + 4) by CARD_1:def 7;

            

             A17: (qP | (NK + 4)) = q by A16, AFINSQ_1: 57;

            (qP . i1) = (q . i1) & (qP . i2) = (q . i2) & (qP . i3) = (q . i3) by A17, HILB10_3: 4;

            then G[qP] & H[qP] by A16, AFINSQ_1: 36, A15;

            then qP in GH;

            hence thesis by A15, A17;

          end;

          hence thesis by A10, A11, XBOOLE_0:def 10;

        end;

        set SN = { ((1 + n) + i) where i be Nat : i in k };

        

         A18: SN c= ( Segm (NK + 4))

        proof

          let x be object;

          assume x in SN;

          then

          consider i be Nat such that

           A19: x = ((1 + n) + i) & i in k;

          i in ( Segm k) by A19;

          then (i + 0 ) < (k + 4) by NAT_1: 44, XREAL_1: 8;

          then ((1 + n) + (i + 0 )) < ((1 + n) + (k + 4)) by XREAL_1: 8;

          hence thesis by A19, NAT_1: 44;

        end;

        set PP = { p where p be (NK + 4) -element XFinSequence of NAT : for i be Nat st i in SN holds T[(p . i), (p . i0), (p . i2), (p . i2)] };

        for i2,i3,i4 be Element of (NK + 4) holds { p where p be (NK + 4) -element XFinSequence of NAT : for i be Nat st i in SN holds T[(p . i), (p . i2), (p . i3), (p . i4)] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from SubsetDioph( A5, A18);

        then

         A20: PP is diophantine Subset of ((NK + 4) -xtuples_of NAT );

        set QQ = { q where q be (NK + 4) -element XFinSequence of NAT : P4[q] };

        

         A21: QQ c= PP

        proof

          let x be object;

          assume x in QQ;

          then

          consider p be (NK + 4) -element XFinSequence of NAT such that

           A22: x = p & P4[p];

          for i be Nat st i in SN holds T[(p . i), (p . i0), (p . i2), (p . i2)]

          proof

            let i be Nat;

            assume i in SN;

            then ex j be Nat st i = ((1 + n) + j) & j in k;

            hence T[(p . i), (p . i0), (p . i2), (p . i2)] by A22;

          end;

          hence thesis by A22;

        end;

        PP c= QQ

        proof

          let x be object;

          assume x in PP;

          then

          consider p be (NK + 4) -element XFinSequence of NAT such that

           A23: x = p & for i be Nat st i in SN holds T[(p . i), (p . i0), (p . i2), (p . i2)];

           P4[p]

          proof

            let i;

            assume i in k;

            then ((1 + n) + i) in SN;

            hence thesis by A23;

          end;

          hence thesis by A23;

        end;

        hence thesis by A20, XBOOLE_0:def 10, A21;

      end;

      defpred P5[ XFinSequence of NAT ] means ($1 . i0) = ((1 * ($1 . ZERO)) + 1);

      

       A24: { q where q be (NK + 4) -element XFinSequence of NAT : P5[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_3: 15;

      defpred P6[ XFinSequence of NAT ] means (1 + ((($1 . i3) + 1) * (($1 . i1) ! ))) = ($1 . i2);

      

       A25: { q where q be (NK + 4) -element XFinSequence of NAT : P6[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_4: 33;

      defpred P7[ XFinSequence of NAT ] means ($1 . i2) = ( Product (1 + ((($1 . i1) ! ) * ( idseq (1 + ($1 . ZERO))))));

      

       A26: { q where q be (NK + 4) -element XFinSequence of NAT : P7[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by HILB10_4: 36;

      reconsider R = p as INT -valued Polynomial of (1 + NK), F_Real ;

      defpred P8[ XFinSequence of NAT ] means for Y be (1 + NK) -element XFinSequence of NAT st Y = ( <%($1 . i3)%> ^ ($1 | NK)) holds (( eval (R,( @ Y))), 0 ) are_congruent_mod ($1 . i2);

      (NK + 0 ) < (NK + 3) by XREAL_1: 8;

      then (NK + 1) <= (NK + 4) & NK in ( Segm i3) by XREAL_1: 8, NAT_1: 44;

      then

       A27: { q where q be (NK + 4) -element XFinSequence of NAT : P8[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) by Th15;

      defpred P123[ XFinSequence of NAT ] means P2[$1] & P3[$1];

      

       A28: { q where q be (NK + 4) -element XFinSequence of NAT : P123[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A2, A3);

      defpred P1234[ XFinSequence of NAT ] means P123[$1] & P4[$1];

      

       A29: { q where q be (NK + 4) -element XFinSequence of NAT : P1234[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A28, A4);

      defpred P12345[ XFinSequence of NAT ] means P1234[$1] & P5[$1];

      

       A30: { q where q be (NK + 4) -element XFinSequence of NAT : P12345[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A29, A24);

      defpred P123456[ XFinSequence of NAT ] means P12345[$1] & P6[$1];

      

       A31: { q where q be (NK + 4) -element XFinSequence of NAT : P123456[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A30, A25);

      defpred P1234567[ XFinSequence of NAT ] means P123456[$1] & P7[$1];

      

       A32: { q where q be (NK + 4) -element XFinSequence of NAT : P1234567[q] } is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A31, A26);

      defpred P12345678[ XFinSequence of NAT ] means P1234567[$1] & P8[$1];

      set X3 = { q where q be (NK + 4) -element XFinSequence of NAT : P12345678[q] };

      

       A33: X3 is diophantine Subset of ((NK + 4) -xtuples_of NAT ) from HILB10_3:sch 3( A32, A27);

      set X2 = { (X | (n + 1)) where X be (NK + 4) -element XFinSequence of NAT : X in X3 };

      (n + 1) <= ((1 + n) + (k + 4)) by NAT_1: 11;

      then

       A34: X2 is diophantine Subset of ((n + 1) -xtuples_of NAT ) by A33, HILB10_3: 5;

      defpred S[ XFinSequence of NAT ] means for z be Element of NAT st z <= ($1 . 0 ) holds ex y be k -element XFinSequence of NAT st for X1 be n -element XFinSequence of NAT st X1 = ($1 /^ 1) holds (for i st i in k holds (y . i) <= ($1 . 0 )) & ( eval (p,( @ (( <%z, ($1 . 0 )%> ^ X1) ^ y)))) = 0 ;

      set X1 = { X where X be (n + 1) -element XFinSequence of NAT : S[X] };

      for s be object holds s in X1 iff s in X2

      proof

        let s be object;

        thus s in X1 implies s in X2

        proof

          assume s in X1;

          then

          consider h be (n + 1) -element XFinSequence of NAT such that

           A35: s = h & S[h];

          set X = (h /^ 1);

          ( len h) = (n + 1) >= 1 by NAT_1: 11, CARD_1:def 7;

          then

           A36: ( len X) = ((n + 1) -' 1) by AFINSQ_2:def 2;

          then

           A37: ( len X) = n by NAT_D: 34;

          reconsider X as n -element XFinSequence of NAT by A36, NAT_D: 34, CARD_1:def 7;

          set x = (h . 0 ), e = (x + 1);

          for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0

          proof

            let z be Element of NAT such that

             A38: z <= x;

            consider y be k -element XFinSequence of NAT such that

             A39: for X1 be n -element XFinSequence of NAT st X1 = (h /^ 1) holds (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X1) ^ y)))) = 0 by A38, A35;

            X = (h /^ 1);

            then (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 by A39;

            hence thesis;

          end;

          then

          consider Y be k -element XFinSequence of NAT , Z,K be Element of NAT such that

           A40: K > x & K >= (sum * ((((x ^2 ) + 1) * ( Product (1 + X))) |^ Deg)) and

           A41: for i be Nat st i in k holds (Y . i) > (x + 1) and

           A42: (1 + ((Z + 1) * (K ! ))) = ( Product (1 + ((K ! ) * ( idseq (x + 1))))) and

           A43: (( eval (p,( @ (( <%Z, x%> ^ X) ^ Y)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))) and

           A44: for i be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq e)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))) by Th17;

          set xXY = (( <%x%> ^ X) ^ Y), E = ((( <%e%> ^ <%K%>) ^ <%(1 + ((Z + 1) * (K ! )))%>) ^ <%Z%>);

          set H = (xXY ^ E);

           0 in ( Segm 1) by NAT_1: 44;

          then

           A45: 0 in ( dom <%x%>) & ( len <%x%>) = 1 & ( dom <%x%>) c= ( dom ( <%x%> ^ X)) by AFINSQ_1: 21, AFINSQ_1: 33;

          then 0 in ( dom ( <%x%> ^ X)) & ( dom ( <%x%> ^ X)) c= ( dom xXY) by AFINSQ_1: 21;

          

          then

           A46: (H . 0 ) = (xXY . 0 ) by AFINSQ_1:def 3

          .= (( <%x%> ^ X) . 0 ) by AFINSQ_1:def 3, A45

          .= ( <%x%> . 0 ) by AFINSQ_1:def 3, A45;

          H = (( <%x%> ^ (X ^ Y)) ^ E) by AFINSQ_1: 27

          .= ( <%x%> ^ ((X ^ Y) ^ E)) by AFINSQ_1: 27;

          

          then

           A47: (H /^ 1) = ((X ^ Y) ^ E) by A45, AFINSQ_2: 12

          .= (X ^ (Y ^ E)) by AFINSQ_1: 27;

          

           A48: ( len xXY) = NK by CARD_1:def 7;

          

           A49: ( len E) = 4 by CARD_1:def 7;

           0 in ( dom E) by AFINSQ_1: 66;

          

          then

           A50: (H . (NK + 0 )) = (E . 0 ) by A48, AFINSQ_1:def 3

          .= e by AFINSQ_1: 45;

          1 in ( dom E) by A49, AFINSQ_1: 66;

          

          then

           A51: (H . (NK + 1)) = (E . 1) by A48, AFINSQ_1:def 3

          .= K by AFINSQ_1: 45;

          2 in ( dom E) by A49, AFINSQ_1: 66;

          

          then

           A52: (H . (NK + 2)) = (E . 2) by A48, AFINSQ_1:def 3

          .= (1 + ((Z + 1) * (K ! ))) by AFINSQ_1: 45;

          3 in ( dom E) by A49, AFINSQ_1: 66;

          

          then

           A53: (H . (NK + 3)) = (E . 3) by A48, AFINSQ_1:def 3

          .= Z by AFINSQ_1: 45;

          

           A54: for i be Nat st i in k holds (H . ((1 + n) + i)) = (Y . i)

          proof

            let i be Nat such that

             A55: i in k;

            

             A56: ( len Y) = k & ( len ( <%x%> ^ X)) = (1 + n) by CARD_1:def 7;

            then ((1 + n) + i) in ( dom xXY) by AFINSQ_1: 23, A55;

            

            hence (H . ((1 + n) + i)) = (xXY . ((1 + n) + i)) by AFINSQ_1:def 3

            .= (Y . i) by A56, A55, AFINSQ_1:def 3;

          end;

          

           A57: for i be Nat st i in k holds (H . ((1 + n) + i)) > (H . NK)

          proof

            let i be Nat such that

             A58: i in k;

            (H . ((1 + n) + i)) = (Y . i) by A58, A54;

            hence thesis by A50, A41, A58;

          end;

          

           A59: for Y be ((2 + n) + k) -element XFinSequence of NAT st Y = ( <%(H . (NK + 3))%> ^ (H | NK)) holds (( eval (p,( @ Y))), 0 ) are_congruent_mod (H . (NK + 2))

          proof

            let YY be ((2 + n) + k) -element XFinSequence of NAT such that

             A60: YY = ( <%(H . (NK + 3))%> ^ (H | NK));

            YY = ( <%(H . (NK + 3))%> ^ xXY) by A48, AFINSQ_1: 57, A60

            .= ( <%Z%> ^ ( <%x%> ^ (X ^ Y))) by A53, AFINSQ_1: 27

            .= (( <%Z%> ^ <%x%>) ^ (X ^ Y)) by AFINSQ_1: 27

            .= (( <%Z, x%> ^ X) ^ Y) by AFINSQ_1: 27;

            hence thesis by A52, A43;

          end;

          

           A61: for i be Nat st i in k holds (( Product (((H . ((1 + n) + i)) + 1) + ( - ( idseq (H . NK))))), 0 ) are_congruent_mod (H . (NK + 2))

          proof

            let i be Nat;

            assume

             A62: i in k;

            then (H . ((1 + n) + i)) = (Y . i) by A54;

            hence thesis by A50, A52, A44, A62;

          end;

          

           A63: P2[H] by A46, A51, A40;

          

           A64: P3[H] by A46, A47, A37, AFINSQ_1: 57, A51, A40;

           P4[H] by A57, A61;

          then H in X3 by A63, A64, A46, A50, A51, A52, A53, A42, A59;

          then

           A66: (H | (n + 1)) in X2;

          (H | (n + 1)) = (xXY | (n + 1)) & ( len ( <%x%> ^ X)) = (1 + n) by NAT_1: 11, A48, AFINSQ_1: 58, CARD_1:def 7;

          then (H | (n + 1)) = ( <%x%> ^ X) by AFINSQ_1: 57;

          hence thesis by A35, A66, NUMERAL2: 2;

        end;

        assume s in X2;

        then

        consider x be (NK + 4) -element XFinSequence of NAT such that

         A67: s = (x | (n + 1)) & x in X3;

        consider H be (NK + 4) -element XFinSequence of NAT such that

         A68: H = x and

         A69: P12345678[H] by A67;

        

         A70: (NK + 4) >= NK & ( len H) = (NK + 4) by NAT_1: 11, CARD_1:def 7;

        then

         A71: ( len (H | NK)) = NK by AFINSQ_1: 54;

        then

         A72: ( len ((H | NK) /^ (n + 1))) = (NK -' (n + 1)) by AFINSQ_2:def 2;

        then

         A73: ( len ((H | NK) /^ (n + 1))) = k by NAT_D: 34;

        reconsider Y = ((H | NK) /^ (n + 1)) as k -element XFinSequence of NAT by A72, CARD_1:def 7, NAT_D: 34;

        reconsider x = (H . 0 ), e = (H . NK), K = (H . (NK + 1)), Z = (H . (NK + 3)) as Element of NAT ;

        

         A74: ( len H) = ((NK + 3) + 1) by CARD_1:def 7;

        then ( len (H /^ 1)) = (((NK + 3) + 1) -' 1) by AFINSQ_2:def 2;

        then

         A75: ( len (H /^ 1)) = (NK + 3) by NAT_D: 34;

        (((1 + k) + 3) + n) >= n by NAT_1: 11;

        then ( len ((H /^ 1) | n)) = n by AFINSQ_1: 54, A75;

        then

        reconsider X = ((H /^ 1) | n) as n -element XFinSequence of NAT by CARD_1:def 7;

        

         A76: for i be Nat st i in k holds (Y . i) = (H . ((1 + n) + i))

        proof

          let i be Nat;

          assume

           A77: i in k;

          then i in ( Segm k);

          then ((1 + n) + i) < ( Segm NK) by NAT_1: 44, XREAL_1: 8;

          then ((H | NK) . ((n + 1) + i)) = (H . ((n + 1) + i)) by NAT_1: 44, FUNCT_1: 49;

          hence thesis by A77, A73, AFINSQ_2:def 2;

        end;

        

         A78: for i be Nat st i in k holds (Y . i) > (x + 1)

        proof

          let i such that

           A79: i in k;

          (Y . i) = (H . ((1 + n) + i)) by A79, A76;

          hence thesis by A79, A69;

        end;

        ( len <%Z%>) = 1 by CARD_1:def 7;

        then ( len ( <%Z%> ^ (H | NK))) = (1 + NK) by A71, AFINSQ_1: 17;

        then

        reconsider ZY = ( <%Z%> ^ (H | NK)) as ((2 + n) + k) -element XFinSequence of NAT by CARD_1:def 7;

        ( Segm (n + 1)) c= ( Segm NK) by NAT_1: 11, NAT_1: 39;

        then

         aa: ((H | NK) | (n + 1)) = (H | (n + 1)) by RELAT_1: 74;

        

         A81: ((1 + 1) -' 1) = 1 & ((n + 2) -' 2) = n by NAT_D: 34;

        (n + 1) <= ((n + 1) + (k + 4)) by NAT_1: 11;

        

        then

         A82: ((H /^ ((1 + 1) -' 1)) | (((n + 1) + 1) -' (1 + 1))) = ( mid (H,(1 + 1),(n + 1))) by A70, AFINSQ_2: 15

        .= ((H | (n + 1)) /^ ((1 + 1) -' 1)) by AFINSQ_2:def 3;

        ( Segm 1) c= ( Segm (n + 1)) by NAT_1: 11, NAT_1: 39;

        

        then ((H | (n + 1)) | 1) = (H | 1) by RELAT_1: 74

        .= <%(H . 0 )%> by NUMERAL2: 1;

        then (H | NK) = (( <%x%> ^ X) ^ Y) by aa, A82, A81;

        

        then ZY = ( <%Z%> ^ ( <%x%> ^ (X ^ Y))) by AFINSQ_1: 27

        .= (( <%Z%> ^ <%x%>) ^ (X ^ Y)) by AFINSQ_1: 27

        .= (( <%Z, x%> ^ X) ^ Y) by AFINSQ_1: 27;

        then

         A83: (( eval (p,( @ (( <%Z, x%> ^ X) ^ Y)))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! ))) by A69;

        

         A84: for i be Nat st i in k holds (( Product (((Y . i) + 1) + ( - ( idseq (x + 1))))), 0 ) are_congruent_mod (1 + ((Z + 1) * (K ! )))

        proof

          let i;

          assume

           A85: i in k;

          then (Y . i) = (H . ((n + 1) + i)) by A76;

          hence thesis by A85, A69;

        end;

        (n + 1) <= ((n + 1) + (k + 4)) by NAT_1: 11;

        then ( len (H | (n + 1))) = (n + 1) by AFINSQ_1: 54, A74;

        then

        reconsider F = (H | (n + 1)) as (n + 1) -element XFinSequence of NAT by CARD_1:def 7;

         0 < ( len F);

        then

         A86: (F . 0 ) = (H . 0 ) by AFINSQ_1: 66, FUNCT_1: 47;

        for z be Element of NAT st z <= (F . 0 ) holds ex y be k -element XFinSequence of NAT st for X1 be n -element XFinSequence of NAT st X1 = (F /^ 1) holds (for i st i in k holds (y . i) <= (F . 0 )) & ( eval (p,( @ (( <%z, (F . 0 )%> ^ X1) ^ y)))) = 0

        proof

          let z be Element of NAT ;

          assume z <= (F . 0 );

          then

          consider y be k -element XFinSequence of NAT such that

           A88: (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ X) ^ y)))) = 0 by A86, A84, Th17, A69, A78, A83;

          take y;

          let X1 be n -element XFinSequence of NAT ;

          assume X1 = (F /^ 1);

          hence thesis by A88, A86, A82, A81;

        end;

        hence thesis by A68, A67;

      end;

      then

       A89: X1 = X2 by TARSKI: 2;

      set Y1 = { (X /^ 1) where X be (n + 1) -element XFinSequence of NAT : X in X1 };

      

       A90: Y1 is diophantine Subset of (n -xtuples_of NAT ) by HILB10_4: 27, A89, A34;

      for s be object holds s in Y1 iff s in X0

      proof

        let s be object;

        thus s in Y1 implies s in X0

        proof

          assume s in Y1;

          then

          consider xS be (n + 1) -element XFinSequence of NAT such that

           A91: s = (xS /^ 1) & xS in X1;

          

           A92: ex w be (n + 1) -element XFinSequence of NAT st xS = w & S[w] by A91;

          ( len xS) = (n + 1) by CARD_1:def 7;

          then ( len (xS /^ 1)) = ((n + 1) -' 1) by AFINSQ_2:def 2;

          then

          reconsider S = (xS /^ 1) as n -element XFinSequence of NAT by NAT_D: 34, CARD_1:def 7;

          ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0

          proof

            take x = (xS . 0 );

            let z be Element of NAT such that

             A93: z <= x;

            consider y be k -element XFinSequence of NAT such that

             A94: for X1 be n -element XFinSequence of NAT st X1 = (xS /^ 1) holds (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, (xS . 0 )%> ^ X1) ^ y)))) = 0 by A92, A93;

            take y;

            S = (xS /^ 1);

            hence thesis by A94;

          end;

          hence thesis by A91;

        end;

        assume s in X0;

        then

        consider S be n -element XFinSequence of NAT such that

         A95: s = S & ex x be Element of NAT st for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0 ;

        consider x be Element of NAT such that

         A96: for z be Element of NAT st z <= x holds ex y be k -element XFinSequence of NAT st (for i st i in k holds (y . i) <= x) & ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0 by A95;

        set xS = ( <%x%> ^ S);

        ( len <%x%>) = 1 by CARD_1:def 7;

        then

         A97: (xS /^ 1) = S by AFINSQ_2: 12;

         S[xS]

        proof

          let z be Element of NAT such that

           A98: z <= (xS . 0 );

          (xS . 0 ) = x by AFINSQ_1: 35;

          then

          consider y be k -element XFinSequence of NAT such that

           A99: (for i st i in k holds (y . i) <= (xS . 0 )) & ( eval (p,( @ (( <%z, x%> ^ S) ^ y)))) = 0 by A96, A98;

          take y;

          thus thesis by A97, AFINSQ_1: 35, A99;

        end;

        then xS in X1;

        hence s in Y1 by A97, A95;

      end;

      hence thesis by A90, TARSKI: 2;

    end;

    ::$Notion-Name

    definition

      let n be Nat;

      let A be Subset of (n -xtuples_of NAT );

      :: HILB10_5:def4

      attr A is recursively_enumerable means ex m be Nat, P be INT -valued Polynomial of ((2 + n) + m), F_Real st for X be n -element XFinSequence of NAT holds X in A iff ex x be Element of NAT st for z be Element of NAT st z <= x holds ex Y be m -element XFinSequence of NAT st (for i be object st i in ( dom Y) holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ X) ^ Y)))) = 0 ;

    end

    theorem :: HILB10_5:20

    for n be Nat holds for A be Subset of (n -xtuples_of NAT ) holds A is diophantine implies A is recursively_enumerable

    proof

      let n be Nat;

      let A be Subset of (n -xtuples_of NAT );

      assume A is diophantine;

      then

      consider m be Nat, P be INT -valued Polynomial of (n + m), F_Real such that

       A1: for s be object holds s in A iff ex x be n -element XFinSequence of NAT , y be m -element XFinSequence of NAT st s = x & ( eval (P,( @ (x ^ y)))) = 0 by HILB10_2:def 6;

      set nm = (n + m);

      reconsider P0 = P as INT -valued Polynomial of ( 0 + nm), F_Real ;

      consider q be Polynomial of (( 0 + 2) + nm), F_Real such that

       A2: ( rng q) c= (( rng P0) \/ {( 0. F_Real )}) and

       A3: for XY be Function of ( 0 + nm), F_Real , XanyY be Function of (( 0 + 2) + nm), F_Real st (XY | 0 ) = (XanyY | 0 ) & (( @ XY) /^ 0 ) = (( @ XanyY) /^ ( 0 + 2)) holds ( eval (P0,XY)) = ( eval (q,XanyY)) by HILB10_2: 28;

      

       A4: ( rng P0) c= INT by RELAT_1:def 19;

      ( 0. F_Real ) in INT by INT_1:def 1;

      then {( 0. F_Real )} c= INT by ZFMISC_1: 31;

      then (( rng P0) \/ {( 0. F_Real )}) c= INT by A4, XBOOLE_1: 8;

      then

      reconsider Q = q as INT -valued Polynomial of ((2 + n) + m), F_Real by RELAT_1:def 19, A2, XBOOLE_1: 1;

      take m, Q;

      let X be n -element XFinSequence of NAT ;

      reconsider S = ( <*> INT ) as 0 -element XFinSequence of NAT ;

      thus X in A implies ex x be Element of NAT st for z be Element of NAT st z <= x holds ex Y be m -element XFinSequence of NAT st (for i be object st i in ( dom Y) holds (Y . i) <= x) & ( eval (Q,( @ (( <%z, x%> ^ X) ^ Y)))) = 0

      proof

        assume X in A;

        then

        consider x be n -element XFinSequence of NAT , y be m -element XFinSequence of NAT such that

         A5: X = x & ( eval (P,( @ (x ^ y)))) = 0 by A1;

        reconsider R = (( rng y) \/ { 0 }) as finite non empty natural-membered set;

        reconsider a = ( max R) as Element of NAT by ORDINAL1:def 12;

        take a;

        let b be Element of NAT such that b <= a;

        take y;

        thus for i be object st i in ( dom y) holds (y . i) <= a

        proof

          let i be object;

          assume i in ( dom y);

          then (y . i) in ( rng y) by FUNCT_1:def 3;

          then (y . i) in R by XBOOLE_0:def 3;

          hence thesis by XXREAL_2:def 8;

        end;

        reconsider A = ( @ (S ^ (x ^ y))) as Function of ( 0 + nm), F_Real ;

        reconsider B = ( @ ((S ^ <%b, a%>) ^ (x ^ y))) as Function of (( 0 + 2) + nm), F_Real ;

        reconsider R = (( rng y) \/ { 0 }) as finite ext-real-membered set;

        

         A6: (A | 0 ) = {} = (B | 0 );

        

         A7: (( @ A) /^ 0 ) = ( @ A) = A = (S ^ (x ^ y)) by AFINSQ_2: 10, HILB10_2:def 1, HILB10_2:def 2;

        ( @ B) = B by HILB10_2:def 2;

        then

         A8: ( @ B) = ((S ^ <%b, a%>) ^ (x ^ y)) by HILB10_2:def 1;

        ( len (S ^ <%b, a%>)) = ( 0 + 2) by CARD_1:def 7;

        then

         A9: (( @ A) /^ 0 ) = (( @ B) /^ ( 0 + 2)) by A7, A8, AFINSQ_2: 12;

        B = ( @ (( <%b, a%> ^ x) ^ y)) by AFINSQ_1: 27;

        hence thesis by A5, A3, A6, A9;

      end;

      given a be Element of NAT such that

       A10: for z be Element of NAT st z <= a holds ex y be m -element XFinSequence of NAT st (for i be object st i in ( dom y) holds (y . i) <= a) & ( eval (Q,( @ (( <%z, a%> ^ X) ^ y)))) = 0 ;

      consider y be m -element XFinSequence of NAT such that

       A11: (for i be object st i in ( dom y) holds (y . i) <= a) & ( eval (Q,( @ (( <%a, a%> ^ X) ^ y)))) = 0 by A10;

      reconsider C = ( @ (S ^ (X ^ y))) as Function of ( 0 + nm), F_Real ;

      reconsider B = ( @ ((S ^ <%a, a%>) ^ (X ^ y))) as Function of (( 0 + 2) + nm), F_Real ;

      

       A12: (C | 0 ) = {} = (B | 0 );

      

       A13: (( @ C) /^ 0 ) = ( @ C) = C = (S ^ (X ^ y)) by AFINSQ_2: 10, HILB10_2:def 1, HILB10_2:def 2;

      ( @ B) = B by HILB10_2:def 2;

      then

       A14: ( @ B) = ((S ^ <%a, a%>) ^ (X ^ y)) by HILB10_2:def 1;

      ( len (S ^ <%a, a%>)) = ( 0 + 2) by CARD_1:def 7;

      then

       A15: (( @ C) /^ 0 ) = (( @ B) /^ ( 0 + 2)) by A13, A14, AFINSQ_2: 12;

      

       A16: B = ( @ (( <%a, a%> ^ X) ^ y)) by AFINSQ_1: 27;

      ( eval (P,( @ (X ^ y)))) = 0 by A11, A16, A3, A12, A15;

      hence thesis by A1;

    end;

    begin

    ::$Notion-Name

    theorem :: HILB10_5:21

    for n be Nat holds for A be Subset of (n -xtuples_of NAT ) holds A is recursively_enumerable implies A is diophantine

    proof

      let n be Nat;

      let A be Subset of (n -xtuples_of NAT );

      assume A is recursively_enumerable;

      then

      consider m be Nat, P be INT -valued Polynomial of ((2 + n) + m), F_Real such that

       A1: for X be n -element XFinSequence of NAT holds X in A iff ex x be Element of NAT st for z be Element of NAT st z <= x holds ex Y be m -element XFinSequence of NAT st (for i be object st i in ( dom Y) holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ X) ^ Y)))) = 0 ;

      set X = { X where X be n -element XFinSequence of NAT : ex x be Element of NAT st for z be Element of NAT st z <= x holds ex Y be m -element XFinSequence of NAT st (for i be Nat st i in m holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ X) ^ Y)))) = 0 };

      

       A2: A c= X

      proof

        let a be object such that

         A3: a in A;

        reconsider a as n -element XFinSequence of NAT by A3, HILB10_2:def 5;

        consider x be Element of NAT such that

         A4: for z be Element of NAT st z <= x holds ex Y be m -element XFinSequence of NAT st (for i be object st i in ( dom Y) holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ a) ^ Y)))) = 0 by A3, A1;

        now

          let z be Element of NAT such that

           A5: z <= x;

          consider Y be m -element XFinSequence of NAT such that

           A6: (for i be object st i in ( dom Y) holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ a) ^ Y)))) = 0 by A4, A5;

          take Y;

          ( len Y) = m by CARD_1:def 7;

          hence (for i be Nat st i in m holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ a) ^ Y)))) = 0 by A6;

        end;

        hence thesis;

      end;

      X c= A

      proof

        let b be object such that

         A7: b in X;

        consider X be n -element XFinSequence of NAT such that

         A8: b = X & ex x be Element of NAT st for z be Element of NAT st z <= x holds ex Y be m -element XFinSequence of NAT st (for i be Nat st i in m holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ X) ^ Y)))) = 0 by A7;

        consider x be Element of NAT such that

         A9: for z be Element of NAT st z <= x holds ex Y be m -element XFinSequence of NAT st (for i be Nat st i in m holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ X) ^ Y)))) = 0 by A8;

        now

          let z be Element of NAT such that

           A10: z <= x;

          consider Y be m -element XFinSequence of NAT such that

           A11: (for i be Nat st i in m holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ X) ^ Y)))) = 0 by A9, A10;

          take Y;

          m = ( len Y) by CARD_1:def 7;

          hence (for i be object st i in ( dom Y) holds (Y . i) <= x) & ( eval (P,( @ (( <%z, x%> ^ X) ^ Y)))) = 0 by A11;

        end;

        hence thesis by A1, A8;

      end;

      then X = A by A2, XBOOLE_0:def 10;

      hence thesis by Th19;

    end;