hilb10_2.miz



    begin

    reserve i,j,k,n,m for Nat,

b,b1,b2 for bag of n;

    registration

      let X be non empty set;

      let n be Nat;

      cluster n -element for XFinSequence of X;

      existence

      proof

        reconsider N0 = (n --> the Element of X) as XFinSequence of X;

        ( len N0) = n by FUNCOP_1: 13;

        then N0 is n -element by CARD_1:def 7;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster n -element real-valued for XFinSequence;

      existence

      proof

        take the n -element XFinSequence of REAL ;

        thus thesis;

      end;

    end

    registration

      let n,m be Nat;

      let p be n -element XFinSequence;

      let q be m -element XFinSequence;

      cluster (p ^ q) -> (n + m) -element;

      coherence

      proof

        ( len (p ^ q)) = (( len p) + ( len q)) & ( len p) = n & ( len q) = m by AFINSQ_1: 17, CARD_1:def 7;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      let p be real-valued XFinSequence;

      let q be real-valued XFinSequence;

      cluster (p ^ q) -> real-valued;

      coherence

      proof

        ( rng (p ^ q)) = (( rng p) \/ ( rng q)) & ( rng p) c= REAL & ( rng q) c= REAL by AFINSQ_1: 26, VALUED_0:def 3;

        hence thesis by VALUED_0:def 3, XBOOLE_1: 8;

      end;

    end

    definition

      let n be Nat;

      let p be n -element real-valued XFinSequence;

      :: HILB10_2:def1

      func @ p -> Function of n, F_Real equals p;

      coherence

      proof

        

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

        ( rng p) c= REAL by VALUED_0:def 3;

        hence thesis by A1, FUNCT_2: 2;

      end;

    end

    definition

      let n be Nat;

      let X be non empty set;

      let p be Function of n, X;

      :: HILB10_2:def2

      func @ p -> n -element XFinSequence of X equals p;

      coherence

      proof

        ( dom p) = n & ( rng p) c= X by FUNCT_2:def 1;

        then

        reconsider P = p as XFinSequence by AFINSQ_1: 5;

        reconsider P as XFinSequence of X;

        ( len P) = n by FUNCT_2:def 1;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      let X be set, p be Permutation of X, M be ManySortedSet of X;

      cluster (M * p) -> total;

      coherence

      proof

        ( dom p) = X & ( rng p) = X & ( dom M) = X by FUNCT_2:def 3, PARTFUN1:def 2;

        then ( dom (M * p)) = X by RELAT_1: 27;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    registration

      let F be finite-support Function;

      let f be one-to-one Function;

      cluster (F * f) -> finite-support;

      coherence

      proof

        ( support (F * f)) c= ((f " ) .: ( support F))

        proof

          let y be object;

          

           A1: ( rng f) = ( dom (f " )) by FUNCT_1: 33;

          assume y in ( support (F * f));

          then

           A2: ((F * f) . y) <> 0 by PRE_POLY:def 7;

          then y in ( dom (F * f)) by FUNCT_1:def 2;

          then ((F * f) . y) = (F . (f . y)) & y in ( dom f) & (f . y) in ( dom F) by FUNCT_1: 11, FUNCT_1: 12;

          then ((f " ) . (f . y)) = y & (f . y) in ( support F) & (f . y) in ( rng f) by A2, PRE_POLY:def 7, FUNCT_1: 34, FUNCT_1:def 3;

          hence thesis by A1, FUNCT_1:def 6;

        end;

        hence thesis by PRE_POLY:def 8;

      end;

    end

    theorem :: HILB10_2:1

    

     Th1: for F,G be XFinSequence st (F ^ G) is one-to-one holds ( rng F) misses ( rng G)

    proof

      let F,G be XFinSequence such that

       A1: (F ^ G) is one-to-one;

      assume ( rng F) meets ( rng G);

      then

      consider y be object such that

       A2: y in ( rng F) & y in ( rng G) by XBOOLE_0: 3;

      consider n1 be object such that

       A3: n1 in ( dom F) & (F . n1) = y by A2, FUNCT_1:def 3;

      consider n2 be object such that

       A4: n2 in ( dom G) & (G . n2) = y by A2, FUNCT_1:def 3;

      reconsider n1, n2 as Nat by A3, A4;

      

       A5: ((F ^ G) . n1) = (F . n1) & ((F ^ G) . (( len F) + n2)) = (G . n2) by A3, A4, AFINSQ_1:def 3;

      ( dom F) c= ( dom (F ^ G)) by AFINSQ_1: 21;

      then n1 in ( dom (F ^ G)) & (( len F) + n2) in ( dom (F ^ G)) by A3, A4, AFINSQ_1: 23;

      then n1 = (n2 + ( len F)) & n1 < ( len F) by A5, A1, FUNCT_1:def 4, A3, A4, AFINSQ_1: 86;

      hence thesis by NAT_1: 11;

    end;

    theorem :: HILB10_2:2

    

     Th2: for X be set, f be X -defined Function, perm be Permutation of X holds ( card ( support (f * perm))) = ( card ( support f))

    proof

      let X be set, f be X -defined Function, perm be Permutation of X;

      set P = (perm " );

      

       A1: ( dom perm) = X = ( rng perm) & ( dom P) = X = ( rng P) by FUNCT_2: 52, FUNCT_2:def 3;

      ( support f) c= ( dom f) c= X = ( dom P) by FUNCT_2: 52, PRE_POLY: 37;

      then

       A2: ( support f) c= ( dom P);

      

       A3: (P .: ( support f)) c= ( support (f * perm))

      proof

        let y be object;

        assume y in (P .: ( support f));

        then

        consider x be object such that

         A4: x in ( dom P) & x in ( support f) & (P . x) = y by FUNCT_1:def 6;

        

         A5: x = (perm . y) by A1, A4, FUNCT_1: 32;

        

         A6: (f . x) <> 0 by A4, PRE_POLY:def 7;

        then x in ( dom f) & y in ( dom perm) by A4, A1, FUNCT_1:def 2, FUNCT_1:def 3;

        then (perm . y) in ( dom f) & (f . (perm . y)) = ((f * perm) . y) by A1, A4, FUNCT_1: 32, FUNCT_1: 13;

        hence thesis by A6, A5, PRE_POLY:def 7;

      end;

      ( support (f * perm)) c= (P .: ( support f))

      proof

        let y be object;

        assume y in ( support (f * perm));

        then

         A7: ((f * perm) . y) <> 0 by PRE_POLY:def 7;

        then y in ( dom (f * perm)) by FUNCT_1:def 2;

        then (f . (perm . y)) = ((f * perm) . y) & y in ( dom perm) & (perm . y) in ( dom f) by FUNCT_1: 11, FUNCT_1: 12;

        then (perm . y) in ( dom P) & (perm . y) in ( support f) & (P . (perm . y)) = y by A1, A7, FUNCT_1: 32, PRE_POLY:def 7;

        hence thesis by FUNCT_1:def 6;

      end;

      then ( support (f * perm)) = (P .: ( support f)) by A3, XBOOLE_0:def 10;

      hence thesis by CARD_1: 5, A2, CARD_1: 33;

    end;

    registration

      let X be set;

      cluster ( 0_ (X, F_Real )) -> natural-valued;

      coherence

      proof

        let x be object;

        assume x in ( dom ( 0_ (X, F_Real )));

        

        then (( 0_ (X, F_Real )) . x) = ( 0. F_Real ) by POLYNOM1: 22

        .= 0 ;

        hence thesis;

      end;

      cluster ( 1_ (X, F_Real )) -> natural-valued;

      coherence

      proof

        let x be object;

        assume

         A1: x in ( dom ( 1_ (X, F_Real )));

        x = ( EmptyBag X) or x <> ( EmptyBag X);

        then (( 1_ (X, F_Real )) . x) = ( 1. F_Real ) or (( 1_ (X, F_Real )) . x) = ( 0. F_Real ) by A1, POLYNOM1: 25;

        hence thesis;

      end;

    end

    registration

      let X be set;

      let x be Element of X;

      cluster ( 1_1 (x, F_Real )) -> natural-valued;

      coherence

      proof

        let a be object;

        assume

         A1: a in ( dom ( 1_1 (x, F_Real )));

        a = ( UnitBag x) or a <> ( UnitBag x);

        then (( 1_1 (x, F_Real )) . a) = ( 1_ F_Real ) or (( 1_1 (x, F_Real )) . a) = ( 0. F_Real ) by A1, HILBASIS: 12;

        hence thesis;

      end;

    end

    registration

      let X be set;

      cluster INT -valued for Series of X, F_Real ;

      existence

      proof

        set x = the Element of X;

        ( 1_1 (x, F_Real )) is INT -valued;

        hence thesis;

      end;

    end

    registration

      let O be Ordinal;

      cluster INT -valued for Polynomial of O, F_Real ;

      existence

      proof

        set x = the Element of O;

        ( 1_1 (x, F_Real )) is INT -valued;

        hence thesis;

      end;

    end

    registration

      let X be set, p be INT -valued Series of X, F_Real ;

      cluster ( - p) -> INT -valued;

      coherence

      proof

        thus ( rng ( - p)) c= INT

        proof

          let y be object such that

           A1: y in ( rng ( - p));

          consider x be object such that

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

          reconsider x as bag of X by A2;

          (( - p) . x) = ( - (p . x)) by POLYNOM1: 17;

          hence thesis by A2, INT_1:def 2;

        end;

      end;

      let q be INT -valued Series of X, F_Real ;

      cluster (p + q) -> INT -valued;

      coherence

      proof

        thus ( rng (p + q)) c= INT

        proof

          let y be object such that

           A3: y in ( rng (p + q));

          consider x be object such that

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

          reconsider x as bag of X by A4;

          ((p + q) . x) = ((p . x) + (q . x)) by POLYNOM1: 15;

          hence thesis by A4, INT_1:def 2;

        end;

      end;

      cluster (p - q) -> INT -valued;

      coherence

      proof

        thus ( rng (p - q)) c= INT

        proof

          let y be object such that

           A5: y in ( rng (p - q));

          consider x be object such that

           A6: x in ( dom (p - q)) & ((p - q) . x) = y by A5, FUNCT_1:def 3;

          reconsider x as bag of X by A6;

          (p - q) = (p + ( - q)) by POLYNOM1:def 7;

          

          then ((p - q) . x) = ((p . x) + (( - q) . x)) by POLYNOM1: 15

          .= ((p . x) + ( - (q . x))) by POLYNOM1: 17;

          hence thesis by A6, INT_1:def 2;

        end;

      end;

    end

    registration

      let X be Ordinal, p,q be INT -valued Series of X, F_Real ;

      cluster (p *' q) -> INT -valued;

      coherence

      proof

        thus ( rng (p *' q)) c= INT

        proof

          let y be object such that

           A1: y in ( rng (p *' q));

          consider x be object such that

           A2: x in ( dom (p *' q)) & ((p *' q) . x) = y by A1, FUNCT_1:def 3;

          reconsider x as bag of X by A2;

          consider s be FinSequence of F_Real such that

           A3: ((p *' q) . x) = ( Sum s) & ( len s) = ( len ( decomp x)) and

           A4: for k be Element of NAT st k in ( dom s) holds ex b1,b2 be bag of X st (( decomp x) /. k) = <*b1, b2*> & (s /. k) = ((p . b1) * (q . b2)) by POLYNOM1:def 10;

          consider f be sequence of F_Real such that

           A5: ( Sum s) = (f . ( len s)) & (f . 0 ) = ( 0. F_Real ) and

           A6: for j be Nat holds for v be Element of F_Real st j < ( len s) & v = (s . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

          defpred P[ Nat] means $1 <= ( len s) implies (f . $1) is integer;

          

           A7: P[ 0 ] by A5;

          

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

          proof

            assume

             A9: P[n];

            set n1 = (n + 1);

            assume

             A10: n1 <= ( len s);

            

             A11: n1 in ( dom s) by A10, FINSEQ_3: 25, NAT_1: 11;

            then

            consider b1,b2 be bag of X such that

             A12: (( decomp x) /. n1) = <*b1, b2*> & (s /. n1) = ((p . b1) * (q . b2)) by A4;

            

             A13: (s /. n1) = (s . n1) by A11, PARTFUN1:def 6;

            (f . n) is integer & (f . n1) = ((f . n) + (s /. n1)) by A9, A6, A13, A10, NAT_1: 13;

            hence thesis by A12;

          end;

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

          then ( Sum s) is integer by A5;

          hence thesis by A3, A2, INT_1:def 2;

        end;

      end;

    end

    registration

      let X be set;

      cluster natural-valued for Function of X, F_Real ;

      existence

      proof

        set A = the Function of X, NAT ;

        

         A1: ( rng A) c= REAL & ( dom A) = X by VALUED_0:def 3, FUNCT_2:def 1;

        reconsider A as Function of X, F_Real by A1, FUNCT_2: 2;

        A is natural-valued;

        hence thesis;

      end;

    end

    registration

      let O be Ordinal;

      cluster INT -valued for Function of O, F_Real ;

      existence

      proof

         the natural-valued Function of O, F_Real is INT -valued;

        hence thesis;

      end;

    end

    registration

      let O be Ordinal;

      let b be bag of O;

      let x be INT -valued Function of O, F_Real ;

      cluster ( eval (b,x)) -> integer;

      coherence

      proof

        reconsider FR = F_Real as well-unital non trivial doubleLoopStr;

        reconsider X = x as Function of O, FR;

        set S = ( SgmX (( RelIncl O),( support b)));

        consider y be FinSequence of the carrier of FR such that

         A1: ( len y) = ( len S) & ( eval (b,X)) = ( Product y) and

         A2: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (( power FR) . (((X * S) /. i),((b * S) /. i))) by POLYNOM2:def 2;

        reconsider Y = y as FinSequence of the carrier of F_Real ;

        

         A3: ( dom y) = ( dom S) by A1, FINSEQ_3: 29;

        defpred P[ Nat] means $1 <= ( len y) implies ( Product (Y | $1)) is integer;

        

         A4: P[ 0 ]

        proof

          (Y | 0 ) = ( <*> the carrier of F_Real );

          then ( Product (Y | 0 )) = ( 1_ F_Real ) by GROUP_4: 8;

          hence thesis;

        end;

        

         A5: (Y | ( len y)) = Y by FINSEQ_1: 58;

        

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

        proof

          assume

           A7: P[n];

          set n1 = (n + 1);

          assume

           A8: n1 <= ( len y);

          then

           A9: n1 in ( dom y) by FINSEQ_3: 25, NAT_1: 11;

          then

           A10: (Y . n1) = (Y /. n1) by PARTFUN1:def 6;

          (Y | n1) = ((Y | n) ^ <*(Y . n1)*>) by A8, NAT_1: 13, FINSEQ_5: 83;

          then

           A11: ( Product (Y | n1)) = (( Product (Y | n)) * (Y /. n1)) by A10, GROUP_4: 6;

          set I = ((x * S) /. n1);

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

          then

           A12: ( rng S) = ( support b) by PRE_POLY:def 2;

          ( dom X) = O by FUNCT_2:def 1;

          then ( dom (X * S)) = ( dom S) by A12, RELAT_1: 27;

          then

           A13: ((X * S) /. n1) = ((X * S) . n1) = I by A3, A9, PARTFUN1:def 6;

          then

           A14: (y /. n1) = (( power F_Real ) . (I,((b * S) /. n1))) by A8, NAT_1: 11, A2;

          reconsider I as Element of F_Real by A13;

          defpred R[ Nat] means (( power F_Real ) . (I,$1)) is integer;

          (( power F_Real ) . (I, 0 )) = ( 1_ F_Real ) by GROUP_1:def 7;

          then

           A15: R[ 0 ];

          

           A16: R[k] implies R[(k + 1)]

          proof

            (( power F_Real ) . (I,(k + 1))) = ((( power F_Real ) . (I,k)) * I) by GROUP_1:def 7;

            hence thesis;

          end;

           R[k] from NAT_1:sch 2( A15, A16);

          then (y /. n1) is integer by A14;

          hence thesis by A11, A8, NAT_1: 13, A7;

        end;

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

        hence thesis by A5, A1;

      end;

    end

    registration

      let O be Ordinal;

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

      let x be INT -valued Function of O, F_Real ;

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

      coherence

      proof

        reconsider FR = F_Real as right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr;

        reconsider X = x as Function of O, FR;

        reconsider P = p as Polynomial of O, FR;

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

        consider y be FinSequence of the carrier of F_Real such that

         A1: ( len y) = ( len S) & ( eval (p,x)) = ( Sum y) and

         A2: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((P * S) /. i) * ( eval ((S /. i),X))) by POLYNOM2:def 4;

        consider f be sequence of F_Real such that

         A3: ( Sum y) = (f . ( len y)) & (f . 0 ) = ( 0. F_Real ) and

         A4: for j be Nat holds for v be Element of F_Real st j < ( len y) & v = (y . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

        defpred P[ Nat] means $1 <= ( len y) implies (f . $1) is integer;

        

         A5: P[ 0 ] by A3;

        

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

        proof

          assume

           A7: P[n];

          set n1 = (n + 1);

          assume

           A8: n1 <= ( len y);

          

           A9: ( dom y) = ( dom S) by A1, FINSEQ_3: 29;

          set I = ((p * S) /. n1);

          ( BagOrder O) linearly_orders ( Support P) by POLYNOM2: 18;

          then

           A10: ( rng S) = ( Support P) by PRE_POLY:def 2;

          ( dom p) = ( Bags O) by FUNCT_2:def 1;

          then

           A11: ( dom (P * S)) = ( dom S) by A10, RELAT_1: 27;

          

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

          then

           A13: ((p * S) /. n1) = ((p * S) . n1) = ((P * S) /. n1) by A11, A9, PARTFUN1:def 6;

          then

          reconsider PP = ((p * S) /. n1) as Element of F_Real ;

          

           A14: (y /. n1) = (PP * ( eval ((S /. n1),x))) by A13, A2, A8, NAT_1: 11;

          (y . n1) = (y /. n1) by A12, PARTFUN1:def 6;

          then (f . n1) = ((f . n) + (y /. n1)) by A4, A8, NAT_1: 13;

          hence thesis by A14, A7, A8, NAT_1: 13;

        end;

         P[n] from NAT_1:sch 2( A5, A6);

        hence thesis by A1, A3;

      end;

    end

    begin

    theorem :: HILB10_2:3

    

     Th3: for b be ManySortedSet of n st k <= n holds (( 0 ,k) -cut b) = (b | k)

    proof

      let b be ManySortedSet of n;

      assume k <= n;

      then

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

      

       A2: ( dom (b | k)) = k by A1, PARTFUN1:def 2;

      

       A3: ( dom (( 0 ,k) -cut b)) = (k -' 0 ) & (k -' 0 ) = k by NAT_D: 40, PARTFUN1:def 2;

      for x be object st x in k holds ((( 0 ,k) -cut b) . x) = ((b | k) . x)

      proof

        let x be object;

        assume

         A4: x in k;

        then x in ( Segm k);

        then

        reconsider n = x as Element of NAT ;

        

        thus ((( 0 ,k) -cut b) . x) = (b . ( 0 + n)) by A4, A3, BAGORDER:def 1

        .= ((b | k) . x) by A4, FUNCT_1: 49;

      end;

      hence thesis by FUNCT_1: 2, A2, A3;

    end;

    theorem :: HILB10_2:4

    

     Th4: for b be bag of (n + 1) holds b = ((( 0 ,n) -cut b) bag_extend (b . n))

    proof

      let b be bag of (n + 1);

      set C = (( 0 ,n) -cut b), B = (C bag_extend (b . n));

      

       A1: (n -' 0 ) = n by NAT_D: 40;

      then

       A2: (B | n) = C & (B . n) = (b . n) by HILBASIS:def 1;

      

       A3: C = (b | n) by Th3, NAT_1: 11;

      

       A4: ( dom b) = (n + 1) = ( dom B) by A1, PARTFUN1:def 2;

      for x be object st x in (n + 1) holds (B . x) = (b . x)

      proof

        let x be object;

        assume x in (n + 1);

        then x in ( Segm (n + 1));

        then x in (( Segm n) \/ {n}) by AFINSQ_1: 2;

        then x in n or x = n by ZFMISC_1: 136;

        then (B . x) = (C . x) = (b . x) or (B . x) = (b . x) by FUNCT_1: 49, A2, A3;

        hence thesis;

      end;

      hence thesis by FUNCT_1: 2, A4;

    end;

    theorem :: HILB10_2:5

    

     Th5: (( 0 ,n) -cut (b bag_extend k)) = b

    proof

      

      thus (( 0 ,n) -cut (b bag_extend k)) = ((b bag_extend k) | n) by Th3, NAT_1: 11

      .= b by HILBASIS:def 1;

    end;

    definition

      let n;

      let L be non empty ZeroStr;

      let p be Series of n, L;

      :: HILB10_2:def3

      func p extended_by_0 -> Series of (n + 1), L means

      : Def3: for b be bag of (n + 1) holds ((b . n) <> 0 implies (it . b) = ( 0. L)) & ((b . n) = 0 implies (it . b) = (p . (( 0 ,n) -cut b)));

      existence

      proof

        defpred P[ Element of ( Bags (n + 1)), Element of L] means (($1 . n) <> 0 implies $2 = ( 0. L)) & (($1 . n) = 0 implies $2 = (p . (( 0 ,n) -cut $1)));

        

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

        proof

          let x be Element of ( Bags (n + 1));

          n = (n -' 0 ) by NAT_D: 40;

          then (( 0 ,n) -cut x) in ( Bags n) by PRE_POLY:def 12;

          then

           A2: (( 0 ,n) -cut x) in ( dom p) by PARTFUN1:def 2;

          per cases ;

            suppose

             A3: (x . n) <> 0 ;

            take ( 0. L);

            thus thesis by A3;

          end;

            suppose

             A4: (x . n) = 0 ;

            take (p /. (( 0 ,n) -cut x));

            thus thesis by A4, A2, PARTFUN1:def 6;

          end;

        end;

        consider f be Function of ( Bags (n + 1)), L such that

         A5: for x be Element of ( Bags (n + 1)) holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let b be bag of (n + 1);

        b is Element of ( Bags (n + 1)) by PRE_POLY:def 12;

        hence thesis by A5;

      end;

      uniqueness

      proof

        let e1,e2 be Series of (n + 1), L such that

         A6: for b be bag of (n + 1) holds ((b . n) <> 0 implies (e1 . b) = ( 0. L)) & ((b . n) = 0 implies (e1 . b) = (p . (( 0 ,n) -cut b))) and

         A7: for b be bag of (n + 1) holds ((b . n) <> 0 implies (e2 . b) = ( 0. L)) & ((b . n) = 0 implies (e2 . b) = (p . (( 0 ,n) -cut b)));

        now

          let b be Element of ( Bags (n + 1));

          (b . n) = 0 or (b . n) <> 0 ;

          then (e1 . b) = ( 0. L) = (e2 . b) or (e1 . b) = (p . (( 0 ,n) -cut b)) = (e2 . b) by A6, A7;

          hence (e1 . b) = (e2 . b);

        end;

        hence thesis;

      end;

    end

    theorem :: HILB10_2:6

    

     Th6: for L be non empty ZeroStr, p be Series of n, L holds ((p extended_by_0 ) . (b bag_extend 0 )) = (p . b)

    proof

      let L be non empty ZeroStr;

      let p be Series of n, L;

      ((b bag_extend 0 ) . n) = 0 by HILBASIS:def 1;

      

      hence ((p extended_by_0 ) . (b bag_extend 0 )) = (p . (( 0 ,n) -cut (b bag_extend 0 ))) by Def3

      .= (p . b) by Th5;

    end;

    theorem :: HILB10_2:7

    

     Th7: for L be non empty ZeroStr, p be Series of n, L, b be bag of (n + 1) st b in ( Support (p extended_by_0 )) holds (b . n) = 0

    proof

      let L be non empty ZeroStr, p be Series of n, L, b be bag of (n + 1);

      assume b in ( Support (p extended_by_0 ));

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

      hence thesis by Def3;

    end;

    theorem :: HILB10_2:8

    

     Th8: for L be non empty ZeroStr, p be Series of n, L holds (b bag_extend 0 ) in ( Support (p extended_by_0 )) iff b in ( Support p)

    proof

      let L be non empty ZeroStr, p be Series of n, L;

      set B = (b bag_extend 0 ), P = (p extended_by_0 );

      (B . n) = 0 by HILBASIS:def 1;

      

      then

       A1: (P . B) = (p . (( 0 ,n) -cut B)) by Def3

      .= (p . b) by Th5;

      thus B in ( Support P) implies b in ( Support p)

      proof

        assume B in ( Support P);

        then (p . b) <> ( 0. L) & b in ( Bags n) & ( dom p) = ( Bags n) by POLYNOM1:def 3, A1, FUNCT_2:def 1, PRE_POLY:def 12;

        hence thesis by POLYNOM1:def 3;

      end;

      assume b in ( Support p);

      then

       A2: (p . b) <> ( 0. L) by POLYNOM1:def 3;

      B in ( Bags (n + 1)) & ( dom P) = ( Bags (n + 1)) by FUNCT_2:def 1;

      hence thesis by POLYNOM1:def 3, A2, A1;

    end;

    theorem :: HILB10_2:9

    

     Th9: for L be non empty ZeroStr, p be Series of n, L, b be bag of (n + 1) st (b . n) = 0 holds b in ( Support (p extended_by_0 )) iff (( 0 ,n) -cut b) in ( Support p)

    proof

      let L be non empty ZeroStr, p be Series of n, L, b be bag of (n + 1);

      assume

       A1: (b . n) = 0 ;

      

       A2: (n -' 0 ) = n by NAT_D: 40;

      b = ((( 0 ,n) -cut b) bag_extend 0 ) by A1, Th4;

      hence thesis by Th8, A2;

    end;

    registration

      let n;

      let L be non empty ZeroStr;

      let p be Polynomial of n, L;

      cluster (p extended_by_0 ) -> finite-Support;

      coherence

      proof

        deffunc F( bag of n) = ($1 bag_extend 0 );

        

         A1: ( Support p) is finite by POLYNOM1:def 5;

        set FS = { F(w) where w be Element of ( Bags n) : w in ( Support p) };

        

         A2: FS is finite from FRAENKEL:sch 21( A1);

        set P = (p extended_by_0 );

        ( Support P) c= FS

        proof

          let x be object;

          assume

           A3: x in ( Support P);

          then

          reconsider b = x as bag of (n + 1);

          

           A4: (n -' 0 ) = n by NAT_D: 40;

          then

          reconsider B = (( 0 ,n) -cut b) as bag of n;

          

           A5: (b . n) = 0 by A3, Th7;

          then B in ( Support p) by A3, Th9;

          then F(B) in FS;

          hence thesis by A4, A5, Th4;

        end;

        hence thesis by A2, POLYNOM1:def 5;

      end;

    end

    theorem :: HILB10_2:10

    

     Th10: for L be non empty ZeroStr, p be Series of n, L holds ( {( 0. L)} \/ ( rng p)) = ( rng (p extended_by_0 ))

    proof

      let L be non empty ZeroStr, p be Series of n, L;

      

       A1: ( dom p) = ( Bags n) & ( dom (p extended_by_0 )) = ( Bags (n + 1)) by FUNCT_2:def 1;

      

       A2: ( rng p) c= ( rng (p extended_by_0 ))

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object such that

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

        reconsider x as Element of ( Bags n) by A3;

        ((p extended_by_0 ) . (x bag_extend 0 )) = (p . x) by Th6;

        hence thesis by A1, FUNCT_1:def 3, A3;

      end;

      set b0 = ( the bag of n bag_extend 1);

      (b0 . n) = 1 by HILBASIS:def 1;

      then

       A4: ((p extended_by_0 ) . b0) = ( 0. L) by Def3;

      ( 0. L) in ( rng (p extended_by_0 )) by A1, A4, FUNCT_1:def 3;

      hence ( {( 0. L)} \/ ( rng p)) c= ( rng (p extended_by_0 )) by A2, ZFMISC_1: 137;

      let y be object;

      assume y in ( rng (p extended_by_0 ));

      then

      consider x be object such that

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

      reconsider x as Element of ( Bags (n + 1)) by A5;

      per cases ;

        suppose (x . n) <> 0 ;

        then y = ( 0. L) by A5, Def3;

        hence thesis by ZFMISC_1: 136;

      end;

        suppose (x . n) = 0 ;

        then

         A6: y = (p . (( 0 ,n) -cut x)) by Def3, A5;

        (n -' 0 ) = n by NAT_D: 40;

        then (( 0 ,n) -cut x) in ( Bags n) by PRE_POLY:def 12;

        then (p . (( 0 ,n) -cut x)) in ( rng p) by A1, FUNCT_1:def 3;

        hence thesis by A6, ZFMISC_1: 136;

      end;

    end;

    theorem :: HILB10_2:11

    

     Th11: ( support b) = ( support (b bag_extend 0 ))

    proof

      set E = (b bag_extend 0 );

      

       A1: b = (E | n) by HILBASIS:def 1;

      thus ( support b) c= ( support E)

      proof

        let x be object;

        assume x in ( support b);

        then

         A2: (b . x) <> 0 by PRE_POLY:def 7;

        then x in ( dom b) by FUNCT_1:def 2;

        then (E . x) = (b . x) by A1, FUNCT_1: 49;

        hence thesis by A2, PRE_POLY:def 7;

      end;

      let x be object;

      assume x in ( support E);

      then

       A3: (E . x) <> 0 by PRE_POLY:def 7;

      then

       A4: x <> n & x in ( dom E) by HILBASIS:def 1, FUNCT_1:def 2;

      ( dom E) = ( Segm (n + 1)) by PARTFUN1:def 2;

      then x in (( Segm n) \/ {n}) by A4, AFINSQ_1: 2;

      then (E . x) = (b . x) by A1, FUNCT_1: 49, A4, ZFMISC_1: 136;

      hence thesis by A3, PRE_POLY:def 7;

    end;

    theorem :: HILB10_2:12

    

     Th12: ( SgmX (( RelIncl n),( support b))) = ( SgmX (( RelIncl (n + 1)),( support (b bag_extend 0 ))))

    proof

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

      set B = (b bag_extend 0 );

      set S2 = ( SgmX (( RelIncl (n + 1)),( support B)));

      

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

      

       A2: ( RelIncl (n + 1)) linearly_orders ( support B) by PRE_POLY: 82;

      

       A3: ( rng S1) = ( support b) & ( rng S2) = ( support B) by A1, A2, PRE_POLY:def 2;

      

       A4: ( support b) = ( support B) by Th11;

      then

      reconsider s2 = S2 as FinSequence of n by A3, FINSEQ_1:def 4;

      reconsider R1 = ( RelIncl (n + 1)) as Order of (n + 1);

      for n1,m1 be Nat st n1 in ( dom s2) & m1 in ( dom s2) & n1 < m1 holds (s2 /. n1) <> (s2 /. m1) & [(s2 /. n1), (s2 /. m1)] in ( RelIncl n)

      proof

        let n1,m1 be Nat such that

         A5: n1 in ( dom s2) & m1 in ( dom s2) & n1 < m1;

         [(S2 /. n1), (S2 /. m1)] in ( RelIncl (n + 1)) by A5, A2, PRE_POLY:def 2;

        then

         A6: (S2 /. n1) c= (S2 /. m1) by WELLORD2:def 1;

        

         A7: (S2 /. n1) = (S2 . n1) = (s2 /. n1) by A5, PARTFUN1:def 6;

        

         A8: (S2 /. m1) = (S2 . m1) = (s2 /. m1) by A5, PARTFUN1:def 6;

        (s2 . n1) in ( rng S2) & (s2 . m1) in ( rng S2) by A5, FUNCT_1:def 3;

        hence thesis by A5, A2, PRE_POLY:def 2, A6, A7, A8, A3, A4, WELLORD2:def 1;

      end;

      hence thesis by A3, A4, A1, PRE_POLY:def 2;

    end;

    theorem :: HILB10_2:13

    

     Th13: for L be well-unital non trivial doubleLoopStr holds for x be Function of n, L, y be Function of (n + 1), L st (y | n) = x holds ( eval (b,x)) = ( eval ((b bag_extend 0 ),y))

    proof

      let L be well-unital non trivial doubleLoopStr;

      let x be Function of n, L, y be Function of (n + 1), L such that

       A1: (y | n) = x;

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

      set B = (b bag_extend 0 );

      set S1 = ( SgmX (( RelIncl (n + 1)),( support B)));

      consider P be FinSequence of L such that

       A2: ( len P) = ( len S) & ( eval (b,x)) = ( Product P) and

       A3: for i be Element of NAT st 1 <= i & i <= ( len P) holds (P /. i) = (( power L) . (((x * S) /. i),((b * S) /. i))) by POLYNOM2:def 2;

      consider P1 be FinSequence of L such that

       A4: ( len P1) = ( len S1) & ( eval (B,y)) = ( Product P1) and

       A5: for i be Element of NAT st 1 <= i & i <= ( len P1) holds (P1 /. i) = (( power L) . (((y * S1) /. i),((B * S1) /. i))) by POLYNOM2:def 2;

      

       A6: S = S1 by Th12;

      

       A7: ( rng S) c= n;

      

       A8: (y * S) = (y * (( id n) * S)) by A7, RELAT_1: 53

      .= ((y * ( id n)) * S) by RELAT_1: 36

      .= (x * S) by RELAT_1: 65, A1;

      

       A9: b = (( 0 ,n) -cut B) by Th5

      .= (B | n) by NAT_1: 11, Th3;

      

       A10: (B * S) = (B * (( id n) * S)) by A7, RELAT_1: 53

      .= ((B * ( id n)) * S) by RELAT_1: 36

      .= (b * S) by A9, RELAT_1: 65;

      for i be Nat st 1 <= i <= ( len P) holds (P . i) = (P1 . i)

      proof

        let i be Nat such that

         A11: 1 <= i <= ( len P);

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

        

         A12: i in ( dom P) & i in ( dom P1) by A2, A4, A6, A11, FINSEQ_3: 25;

        then (P /. I) = (P . i) by PARTFUN1:def 6;

        

        hence (P . i) = (( power L) . (((y * S1) /. i),((B * S1) /. i))) by A3, A11, A6, A8, A10

        .= (P1 /. I) by A5, A11, A2, A4, A6

        .= (P1 . i) by A12, PARTFUN1:def 6;

      end;

      hence thesis by A2, A4, A6, FINSEQ_1: 14;

    end;

    theorem :: HILB10_2:14

    

     Th14: b1 < b2 iff (b1 bag_extend k) < (b2 bag_extend k)

    proof

      set B1 = (b1 bag_extend k), B2 = (b2 bag_extend k);

      

       A1: (B1 | n) = b1 & (B2 | n) = b2 & (B1 . n) = k = (B2 . n) by HILBASIS:def 1;

      

       A2: ( dom b2) = n = ( dom b1) by PARTFUN1:def 2;

      thus b1 < b2 implies (b1 bag_extend k) < (b2 bag_extend k)

      proof

        assume b1 < b2;

        then

        consider o be Ordinal such that

         A3: (b1 . o) < (b2 . o) and

         A4: for l be Ordinal st l in o holds (b1 . l) = (b2 . l) by PRE_POLY:def 9;

        

         A5: o in ( dom b2) by A3, FUNCT_1:def 2;

        then

         A6: (B2 . o) = (b2 . o) & (B1 . o) = (b1 . o) by A1, FUNCT_1: 47, A2;

        for l be Ordinal st l in o holds (B1 . l) = (B2 . l)

        proof

          let l be Ordinal;

          assume

           A7: l in o;

          then (B2 . l) = (b2 . l) & (B1 . l) = (b1 . l) by A1, FUNCT_1: 47, A2, A5, ORDINAL1: 10;

          hence thesis by A7, A4;

        end;

        hence thesis by A3, A6, PRE_POLY:def 9;

      end;

      assume B1 < B2;

      then

      consider o be Ordinal such that

       A8: (B1 . o) < (B2 . o) and

       A9: for l be Ordinal st l in o holds (B1 . l) = (B2 . l) by PRE_POLY:def 9;

      o in ( dom B2) by A8, FUNCT_1:def 2;

      then o in ( Segm (n + 1));

      then o in (( Segm n) \/ {n}) by AFINSQ_1: 2;

      then

       A10: o in n or o = n by ZFMISC_1: 136;

      then

       A11: (B2 . o) = (b2 . o) & (B1 . o) = (b1 . o) by A1, A8, FUNCT_1: 47, A2;

      for l be Ordinal st l in o holds (b1 . l) = (b2 . l)

      proof

        let l be Ordinal;

        assume

         A12: l in o;

        then (B2 . l) = (b2 . l) & (B1 . l) = (b1 . l) by A2, A10, A1, FUNCT_1: 47, ORDINAL1: 10;

        hence thesis by A12, A9;

      end;

      hence thesis by A8, A11, PRE_POLY:def 9;

    end;

    theorem :: HILB10_2:15

    for X be non empty set, A be finite Subset of X, R be Order of X st R linearly_orders A holds for i, k st 1 <= i <= k <= ( card A) holds (( SgmX (R,( rng (( SgmX (R,A)) | k)))) /. i) = (( SgmX (R,A)) /. i)

    proof

      let X be non empty set, A be finite Subset of X, R be Order of X;

      assume

       A1: R linearly_orders A;

      set Sp = ( SgmX (R,A));

      

       A2: ( card A) = ( len Sp) by A1, PRE_POLY: 11;

      

       A3: ( rng Sp) = A by A1, PRE_POLY:def 2;

      defpred P[ Nat] means for i st 1 <= i <= $1 <= ( card A) holds (( SgmX (R,( rng (Sp | $1)))) /. i) = (Sp /. i);

      

       A4: P[ 0 ];

      

       A5: for k st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        set k1 = (k + 1);

        assume

         A6: P[k];

        let i be Nat such that

         A7: 1 <= i <= k1 <= ( card A);

        

         A8: Sp is one-to-one by A1, PRE_POLY: 10;

        set Spk1 = (Sp | k1);

        

         A9: k < ( card A) by A7, NAT_1: 13;

        then

         A10: ( len Spk1) = k1 & ( len (Sp | k)) = k by A7, A2, FINSEQ_1: 59;

        

         A11: k < ( len Sp) by A7, A2, NAT_1: 13;

        

         A12: Spk1 = ((Sp | k) ^ <*(Sp . k1)*>) by A7, A2, NAT_1: 13, FINSEQ_5: 83;

        

         A13: R linearly_orders ( rng (Sp | k1)) by A3, RELAT_1: 70, A1, ORDERS_1: 38;

        

         A14: 1 <= k1 by NAT_1: 11;

        

         A15: k1 in ( dom Sp) by NAT_1: 11, A7, A2, FINSEQ_3: 25;

        then

         A16: (Sp . k1) in ( rng Sp) by FUNCT_1:def 3;

        

         A17: (Sp . k1) = (Sp /. k1) by A15, PARTFUN1:def 6;

        

         A18: k1 in ( Seg k1) by A14;

        

         A19: (Sp /. k1) in ( rng Spk1) by A15, A18, PARTFUN2: 18;

        

         A20: for y be Element of X st y in ( rng (Sp | k1)) holds [y, (Sp /. k1)] in R

        proof

          let y be Element of X such that

           A21: y in ( rng Spk1);

          consider w be object such that

           A22: w in ( dom Spk1) & (Spk1 . w) = y by A21, FUNCT_1:def 3;

          reconsider w as Nat by A22;

          

           A23: 1 <= w <= k1 by A22, A10, FINSEQ_3: 25;

          then

           A24: (Spk1 . w) = (Sp . w) by FINSEQ_3: 112;

          w <= ( len Sp) by A7, A2, A23, XXREAL_0: 2;

          then

           A25: w in ( dom Sp) by A23, FINSEQ_3: 25;

          then

           A26: (Sp /. w) = (Sp . w) by PARTFUN1:def 6;

          per cases by A23, XXREAL_0: 1;

            suppose

             A27: w = k1;

            R is_reflexive_in A by A1, ORDERS_1:def 9;

            hence [y, (Sp /. k1)] in R by A27, A17, A24, A22, A3, A16;

          end;

            suppose w < k1;

            hence [y, (Sp /. k1)] in R by A22, A24, A26, A25, A15, A1, PRE_POLY:def 2;

          end;

        end;

        

         A28: ( len ( SgmX (R,( rng (Sp | k1))))) = ( card ( rng (Sp | k1))) by A13, PRE_POLY: 11

        .= k1 by A10, A8, FINSEQ_4: 62;

        

         A29: not (Sp /. k1) in ( rng (Sp | k))

        proof

          assume (Sp /. k1) in ( rng (Sp | k));

          then

          consider w be object such that

           A30: w in ( dom (Sp | k)) & ((Sp | k) . w) = (Sp /. k1) by FUNCT_1:def 3;

          reconsider w as Nat by A30;

          

           A31: 1 <= w <= k by A30, A10, FINSEQ_3: 25;

          w <= ( len Sp) by A9, A2, A31, XXREAL_0: 2;

          then

           A32: w in ( dom Sp) by A31, FINSEQ_3: 25;

          (Sp . w) = (Sp . k1) by A30, A31, FINSEQ_3: 112, A17;

          then w = k1 by A8, A15, A32, FUNCT_1:def 4;

          hence thesis by A31, NAT_1: 13;

        end;

        ( rng Spk1) = (( rng (Sp | k)) \/ ( rng <*(Sp . k1)*>)) by A12, FINSEQ_1: 31

        .= (( rng (Sp | k)) \/ {(Sp . k1)}) by FINSEQ_1: 38;

        then

         A33: ( rng (Sp | k1)) = ( {(Sp /. k1)} \/ ( rng (Sp | k))) by A15, PARTFUN1:def 6;

        

         A34: k1 in ( dom ( SgmX (R,( rng (Sp | k1))))) by A14, A28, FINSEQ_3: 25;

        (( SgmX (R,( rng (Sp | k1)))) /. k1) = (Sp /. k1) by A28, A20, A19, A13, PRE_POLY: 21;

        then

         A35: for i be Element of NAT st 1 <= i & i <= (k1 - 1) holds (( SgmX (R,( rng (Sp | k)))) /. i) = (( SgmX (R,( rng (Sp | k1)))) /. i) by A13, A29, A33, A34, PRE_POLY: 78;

        

         A36: i in NAT by ORDINAL1:def 12;

        per cases by A7, XXREAL_0: 1;

          suppose i < k1;

          then

           A37: i <= k by NAT_1: 13;

          

          hence (( SgmX (R,( rng (Sp | k1)))) /. i) = (( SgmX (R,( rng (Sp | k)))) /. i) by A36, A7, A35

          .= (Sp /. i) by A11, A6, A37, A7, A2;

        end;

          suppose i = k1;

          hence thesis by A20, A28, A19, A13, PRE_POLY: 21;

        end;

      end;

      for k holds P[k] from NAT_1:sch 2( A4, A5);

      hence thesis;

    end;

    theorem :: HILB10_2:16

    

     Th16: for O be Ordinal, A be finite Subset of ( Bags O) st n in ( dom ( SgmX (( BagOrder O),A))) & m in ( dom ( SgmX (( BagOrder O),A))) & n < m holds (( SgmX (( BagOrder O),A)) /. n) < (( SgmX (( BagOrder O),A)) /. m)

    proof

      let O be Ordinal, A be finite Subset of ( Bags O);

      set S = ( SgmX (( BagOrder O),A));

      assume

       A1: n in ( dom S) & m in ( dom S) & n < m;

      ( BagOrder O) linearly_orders ( field ( BagOrder O)) by ORDERS_1: 37;

      then ( BagOrder O) linearly_orders ( Bags O) by ORDERS_1: 12;

      then ( BagOrder O) linearly_orders A by ORDERS_1: 38;

      then

       A2: (S /. n) <> (S /. m) & [(S /. n), (S /. m)] in ( BagOrder O) by PRE_POLY:def 2, A1;

      then (S /. n) <=' (S /. m) by PRE_POLY:def 14;

      hence thesis by A2, PRE_POLY:def 10;

    end;

    theorem :: HILB10_2:17

    

     Th17: for L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr holds for p be Polynomial of n, L holds ( len ( SgmX (( BagOrder n),( Support p)))) = ( len ( SgmX (( BagOrder (n + 1)),( Support (p extended_by_0 ))))) & for i be Nat st 1 <= i <= ( len ( SgmX (( BagOrder n),( Support p)))) holds (( SgmX (( BagOrder (n + 1)),( Support (p extended_by_0 )))) /. i) = ((( SgmX (( BagOrder n),( Support p))) /. i) bag_extend 0 )

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr;

      let p be Polynomial of n, L;

      set B = ( BagOrder n), B1 = ( BagOrder (n + 1));

      set P = (p extended_by_0 );

      

       A1: (n -' 0 ) = n by NAT_D: 40;

      

       A2: B linearly_orders ( Support p) & B1 linearly_orders ( Support P) by POLYNOM2: 18;

      deffunc F( bag of n) = ($1 bag_extend 0 );

      

       A3: for x be Element of ( Bags n) holds F(x) in ( Bags (n + 1));

      consider f be Function of ( Bags n), ( Bags (n + 1)) such that

       A4: for x be Element of ( Bags n) holds (f . x) = F(x) from FUNCT_2:sch 8( A3);

      set F = (f | ( Support p));

      

       A5: ( dom F) = ( Support p) by FUNCT_2:def 1;

      set Sp = ( SgmX (B,( Support p))), SP = ( SgmX (B1,( Support P)));

      

       A6: ( rng F) c= ( Support P)

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A7: x in ( dom F) & (F . x) = y by FUNCT_1:def 3;

        reconsider x as Element of ( Bags n) by A7, A5;

        

         A8: (f . x) = (F . x) by A7, FUNCT_1: 47;

        (f . x) = F(x) by A4;

        hence thesis by A7, A8, Th8;

      end;

      ( Support P) c= ( rng F)

      proof

        let y be object;

        assume

         A9: y in ( Support P);

        then

        reconsider b = y as bag of (n + 1);

        set C = (( 0 ,n) -cut b);

        

         A10: (b . n) = 0 by A9, Th7;

        then

         A11: C in ( Support p) by A9, Th9;

        then

        reconsider C as Element of ( Bags n);

         F(C) = (f . C) = (F . C) by A11, A4, FUNCT_1: 49;

        then

         A12: F(C) in ( rng F) by A11, A5, FUNCT_1:def 3;

        (n -' 0 ) = n by NAT_D: 40;

        hence thesis by A12, A10, Th4;

      end;

      then

       A13: ( Support P) = ( rng F) by A6, XBOOLE_0:def 10;

      F is one-to-one

      proof

        let x1,x2 be object;

        assume

         A14: x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2);

        reconsider x1, x2 as Element of ( Bags n) by A14, A5;

        

         A15: (f . x1) = (F . x1) & (f . x2) = (F . x2) by A14, FUNCT_1: 47;

        (f . x1) = F(x1) & (f . x2) = F(x2) by A4;

        then F(x1) = F(x2) & x1 = ( F(x1) | n) by HILBASIS:def 1, A15, A14;

        hence thesis by HILBASIS:def 1;

      end;

      then

       A16: ( len Sp) = ( card ( Support p)) = ( card ( Support P)) = ( len SP) by CARD_1: 5, POLYNOM2: 18, PRE_POLY: 11, A5, A13, WELLORD2:def 4;

      hence ( len Sp) = ( len SP);

      defpred P[ Nat] means 1 <= $1 <= ( len Sp) implies for i st 1 <= i <= $1 holds (SP /. i) = ((Sp /. i) bag_extend 0 );

      

       A17: ( rng Sp) = ( Support p) & ( rng SP) = ( Support P) by A2, PRE_POLY:def 2;

      

       A18: P[ 0 ];

      

       A19: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        set k1 = (k + 1);

        assume that

         A20: P[k] and

         A21: 1 <= k1 <= ( len Sp);

        let i be Nat such that

         A22: 1 <= i <= k1;

        

         A23: k < ( len Sp) by A21, NAT_1: 13;

        

         A24: k = ( len (SP | k)) by A23, A16, FINSEQ_1: 59;

        

         A25: ( rng (Sp | k1)) c= ( Support p) & ( rng (SP | k1)) c= ( Support P) by A17, RELAT_1: 70;

        

         A26: (Sp | k1) = ((Sp | k) ^ <*(Sp . k1)*>) & (SP | k1) = ((SP | k) ^ <*(SP . k1)*>) by A16, A21, NAT_1: 13, FINSEQ_5: 83;

        

         A27: k1 in ( dom Sp) & k1 in ( dom SP) by A21, A16, FINSEQ_3: 25;

        then

         A28: (Sp . k1) in ( rng Sp) & (SP . k1) in ( rng SP) by FUNCT_1:def 3;

        

         A29: (Sp . k1) = (Sp /. k1) & (SP . k1) = (SP /. k1) by A27, PARTFUN1:def 6;

        per cases by NAT_1: 14;

          suppose

           A30: k = 0 ;

          

           A31: i = 1 by A30, A22, XXREAL_0: 1;

          

           A32: ((Sp /. 1) bag_extend 0 ) in ( Support P) by Th8, A30, A29, A28, A17;

          for y be Element of ( Bags (n + 1)) st y in ( Support P) holds [((Sp /. 1) bag_extend 0 ), y] in B1

          proof

            let y be Element of ( Bags (n + 1));

            set Y = (( 0 ,n) -cut y);

            assume

             A33: y in ( Support P);

            then (y . n) = 0 by Th7;

            then Y in ( Support p) by A33, Th9;

            then

            consider w be object such that

             A34: w in ( dom Sp) & (Sp . w) = Y by FUNCT_1:def 3, A17;

            (y . n) = 0 by Th7, A33;

            then

             A35: y = (Y bag_extend 0 ) by Th4;

            reconsider w as Nat by A34;

            

             A36: (Sp . w) = (Sp /. w) by A34, PARTFUN1:def 6;

            

             A37: 1 <= w by A34, FINSEQ_3: 25;

            per cases by A37, XXREAL_0: 1;

              suppose w = 1;

              hence thesis by PRE_POLY:def 14, A35, A1, A34, A36;

            end;

              suppose w > 1;

              then

               A38: (Sp /. 1) <> (Sp /. w) & [(Sp /. 1), (Sp /. w)] in B by A2, PRE_POLY:def 2, A27, A34, A30;

              then (Sp /. 1) <=' (Sp /. w) by PRE_POLY:def 14;

              then ((Sp /. 1) bag_extend 0 ) < ((Sp /. w) bag_extend 0 ) by Th14, A38, PRE_POLY:def 10;

              then ((Sp /. 1) bag_extend 0 ) <=' y by A1, A34, A36, A35, PRE_POLY:def 10;

              hence thesis by PRE_POLY:def 14;

            end;

          end;

          hence (SP /. i) = ((Sp /. i) bag_extend 0 ) by A31, A32, POLYNOM2: 18, PRE_POLY: 20;

        end;

          suppose

           A39: k >= 1;

          

           A40: k1 in ( Seg k1) by A21;

          set Ck = (( 0 ,n) -cut (SP /. k1));

          reconsider Ck as bag of n by A1;

          

           A41: (SP /. k1) in ( rng (SP | k1)) by PARTFUN2: 18, A40, A27;

          then

           A42: ((SP /. k1) . n) = 0 by Th7, A25;

          then Ck in ( Support p) by Th9, A41, A25;

          then

          consider f be object such that

           A43: f in ( dom Sp) & (Sp . f) = Ck by FUNCT_1:def 3, A17;

          reconsider f as Nat by A43;

          

           A44: (Sp /. f) = (Sp . f) by A43, PARTFUN1:def 6;

          

           A45: (SP /. k1) = (Ck bag_extend 0 ) by A1, A42, Th4;

          set SpEk = ((Sp /. k1) bag_extend 0 );

          SpEk in ( Support P) by A29, A28, A17, Th8;

          then

          consider e be object such that

           A46: e in ( dom SP) & (SP . e) = SpEk by FUNCT_1:def 3, A17;

          reconsider e as Nat by A46;

          

           A47: 1 <= e <= ( len SP) by FINSEQ_3: 25, A46;

          

           A48: (SP /. e) = (SP . e) by A46, PARTFUN1:def 6;

          

           A49: (SP /. k) = ((Sp /. k) bag_extend 0 ) by A20, A39, A21, NAT_1: 13;

          

           A50: SpEk in ( rng (SP | k1))

          proof

            assume

             A51: not SpEk in ( rng (SP | k1));

            e > k1

            proof

              assume e <= k1;

              then e in ( Seg k1) by A47;

              hence thesis by A51, A48, A46, PARTFUN2: 18;

            end;

            then

             A52: (Sp /. f) < (Sp /. k1) by A43, A44, Th14, A46, A27, A45, A48, Th16;

            

             A53: k in ( dom SP) & k in ( dom Sp) by A23, A39, A16, FINSEQ_3: 25;

            

             A54: k < k1 by NAT_1: 13;

            

             A55: (Sp /. k) < (Sp /. f) by A43, A44, Th14, A49, A45, Th16, A27, A53, A54;

            then

             A56: k <> f;

            per cases ;

              suppose k <= f;

              then k < f by A56, XXREAL_0: 1;

              then k1 <= f & k1 <> f by A52, NAT_1: 13;

              then k1 < f by XXREAL_0: 1;

              hence thesis by A52, A43, A27, Th16;

            end;

              suppose k > f;

              hence thesis by A55, A43, A53, Th16;

            end;

          end;

          

           A57: ( rng (SP | k1)) = (( rng (SP | k)) \/ ( rng <*(SP . k1)*>)) by A26, FINSEQ_1: 31

          .= (( rng (SP | k)) \/ {(SP . k1)}) by FINSEQ_1: 38;

          

           A58: SpEk = (SP . k1)

          proof

            assume SpEk <> (SP . k1);

            then SpEk in ( rng (SP | k)) by A50, A57, ZFMISC_1: 136;

            then

            consider w be object such that

             A59: w in ( dom (SP | k)) & ((SP | k) . w) = SpEk by FUNCT_1:def 3;

            reconsider w as Nat by A59;

            

             A60: 1 <= w <= k by A24, FINSEQ_3: 25, A59;

            then w < ( len Sp) by A23, XXREAL_0: 2;

            then

             A61: w in ( dom Sp) & w in ( dom SP) by A16, A60, FINSEQ_3: 25;

            

             A62: (SP /. w) = ((Sp /. w) bag_extend 0 ) by A39, A20, A21, NAT_1: 13, A60;

            

             A63: (SP /. w) = (SP . w) = ((SP | k) . w) = SpEk by A59, A60, A61, PARTFUN1:def 6, FINSEQ_3: 112;

            w < k1 by A60, NAT_1: 13;

            then ((Sp /. w) bag_extend 0 ) < ((Sp /. k1) bag_extend 0 ) by A27, A61, Th14, Th16;

            hence thesis by A62, A63;

          end;

          per cases by A22, XXREAL_0: 1;

            suppose i < k1;

            then i <= k by NAT_1: 13;

            hence thesis by A22, A20, A21, NAT_1: 13, A39;

          end;

            suppose i = k1;

            hence (SP /. i) = ((Sp /. i) bag_extend 0 ) by A58, A27, PARTFUN1:def 6;

          end;

        end;

      end;

      for k holds P[k] from NAT_1:sch 2( A18, A19);

      hence thesis;

    end;

    theorem :: HILB10_2:18

    

     Th18: for L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, x be Function of n, L, y be Function of (n + 1), L st (y | n) = x holds ( eval (p,x)) = ( eval ((p extended_by_0 ),y))

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, x be Function of n, L, y be Function of (n + 1), L;

      set n1 = (n + 1);

      assume

       A1: (y | n) = x;

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

      set P = (p extended_by_0 );

      set S1 = ( SgmX (( BagOrder n1),( Support P)));

      consider T be FinSequence of L such that

       A2: ( len T) = ( len S) & ( eval (p,x)) = ( Sum T) and

       A3: for i be Element of NAT st 1 <= i & i <= ( len T) holds (T /. i) = (((p * S) /. i) * ( eval ((S /. i),x))) by POLYNOM2:def 4;

      consider T1 be FinSequence of L such that

       A4: ( len T1) = ( len S1) & ( eval (P,y)) = ( Sum T1) and

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

      

       A6: ( len S) = ( len S1) & for i be Nat st 1 <= i <= ( len S) holds (S1 /. i) = ((S /. i) bag_extend 0 ) by Th17;

      ( BagOrder n) linearly_orders ( Support p) & ( BagOrder n1) linearly_orders ( Support P) by POLYNOM2: 18;

      then

       A7: ( rng S) = ( Support p) & ( rng S1) = ( Support P) by PRE_POLY:def 2;

      ( dom p) = ( Bags n) & ( dom P) = ( Bags n1) by FUNCT_2:def 1;

      then

       A8: ( dom (p * S)) = ( dom S) & ( dom (P * S1)) = ( dom S1) by A7, RELAT_1: 27;

      for i be Nat st 1 <= i <= ( len S) holds (T . i) = (T1 . i)

      proof

        let i such that

         A9: 1 <= i <= ( len S);

        

         A10: i in NAT by ORDINAL1:def 12;

        

         A11: i in ( dom T) & i in ( dom T1) by A9, A6, A2, A4, FINSEQ_3: 25;

        

         A12: i in ( dom S) & i in ( dom S1) by A9, A6, FINSEQ_3: 25;

        then

         A13: (S /. i) = (S . i) & (S1 /. i) = (S1 . i) by PARTFUN1:def 6;

        

         A14: (S1 /. i) = ((S /. i) bag_extend 0 ) by Th17, A9;

        

         A15: ((P * S1) /. i) = ((P * S1) . i) by A9, A6, FINSEQ_3: 25, A8, PARTFUN1:def 6

        .= (P . (S1 /. i)) by A12, A13, FUNCT_1: 13

        .= (P . ((S /. i) bag_extend 0 )) by Th17, A9

        .= (p . (S /. i)) by Th6

        .= (p . (S . i)) by A12, PARTFUN1:def 6

        .= ((p * S) . i) by A12, FUNCT_1: 13

        .= ((p * S) /. i) by A9, FINSEQ_3: 25, A8, PARTFUN1:def 6;

        

        thus (T1 . i) = (T1 /. i) by A11, PARTFUN1:def 6

        .= (((P * S1) /. i) * ( eval ((S1 /. i),y))) by A10, A5, A9, A4, A6

        .= (((p * S) /. i) * ( eval ((S /. i),x))) by A14, Th13, A1, A15

        .= (T /. i) by A10, A3, A9, A2

        .= (T . i) by A11, PARTFUN1:def 6;

      end;

      hence thesis by FINSEQ_1: 14, A2, A4, Th17;

    end;

    begin

    theorem :: HILB10_2:19

    

     Th19: for O be Ordinal, L be well-unital commutative associative non trivial doubleLoopStr, x be Function of O, L, b be bag of O holds for S be one-to-one FinSequence of O st ( rng S) = ( support b) holds ex y be FinSequence of L st ( len y) = ( card ( support b)) & ( eval (b,x)) = ( Product y) & for i st 1 <= i & i <= ( len y) holds (y /. i) = (( power L) . (((x * S) /. i),((b * S) /. i)))

    proof

      let n be Ordinal, L be well-unital commutative associative non trivial doubleLoopStr, x be Function of n, L, b be bag of n;

      let S be one-to-one FinSequence of n such that

       A1: ( rng S) = ( support b);

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

      consider y be FinSequence of L such that

       A2: ( len y) = ( len SG) & ( eval (b,x)) = ( Product y) and

       A3: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (( power L) . (((x * SG) /. i),((b * SG) /. i))) by POLYNOM2:def 2;

      

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

      

       A5: SG is one-to-one & ( len SG) = ( card ( support b)) by PRE_POLY: 10, PRE_POLY: 11, PRE_POLY: 82;

      

       A6: ( rng SG) = ( support b) by A4, PRE_POLY:def 2;

      then

      consider H be Function such that

       A7: ( dom H) = ( dom S) & ( rng H) = ( dom SG) & H is one-to-one & (SG * H) = S by A1, A5, RFINSEQ: 26, CLASSES1: 77;

      

       A8: ( len S) = ( len SG) by A1, A5, A6, FINSEQ_1: 48;

      

       A9: ( dom y) = ( dom SG) = ( dom S) by A2, A8, FINSEQ_3: 29;

      then

       A10: ( dom (y * H)) = ( dom H) & ( dom S) = ( Seg ( len S)) by A7, RELAT_1: 27, FINSEQ_1:def 3;

      then

      reconsider yH = (y * H) as FinSequence by A7, FINSEQ_1:def 2;

      reconsider H as Function of ( dom y), ( dom y) by A7, A9, FUNCT_2: 1;

      H is onto by A7, A2, FINSEQ_3: 29;

      then

      reconsider H as Permutation of ( dom y) by A7;

      

       A11: ( rng y) c= the carrier of L;

      ( rng yH) c= ( rng y) by RELAT_1: 26;

      then ( rng yH) c= the carrier of L by A11;

      then

      reconsider yH as FinSequence of L by FINSEQ_1:def 4;

      take yH;

      thus ( len yH) = ( card ( support b)) by A7, A10, FINSEQ_3: 29, A8, A5;

      

       A12: H is Permutation of ( dom y);

      

      thus ( eval (b,x)) = (the multF of L "**" y) by GROUP_4:def 2, A2

      .= (the multF of L "**" yH) by FINSOP_1: 7, A12

      .= ( Product yH) by GROUP_4:def 2;

      let i be Nat such that

       A13: 1 <= i & i <= ( len yH);

      set Hi = (H /. i);

      i in ( dom yH) by A13, FINSEQ_3: 25;

      then

       A14: (yH /. i) = (yH . i) & (H . i) = Hi & (yH . i) = (y . (H . i)) & (H . i) in ( rng H) by A10, PARTFUN1:def 6, FUNCT_1: 12, FUNCT_1:def 3;

      then

       A15: 1 <= Hi <= ( len y) & Hi in NAT & (y . Hi) = (y /. Hi) by FINSEQ_3: 25, PARTFUN1:def 6;

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

      then ( rng SG) c= ( dom x) & ( rng S) c= ( dom x);

      then

       A16: ( dom (x * SG)) = ( dom SG) & ( dom (x * S)) = ( dom S) by RELAT_1: 27;

      

      then

       A17: ((x * SG) /. Hi) = ((x * SG) . Hi) by A14, A7, PARTFUN1:def 6

      .= (x . (SG . Hi)) by A16, A14, A7, FUNCT_1: 12

      .= (x . ((SG * H) . i)) by A14, A13, FINSEQ_3: 25, A7, A10, FUNCT_1: 12

      .= ((x * S) . i) by A7, A16, A13, FINSEQ_3: 25, A10, FUNCT_1: 12

      .= ((x * S) /. i) by A7, A16, A13, FINSEQ_3: 25, A10, PARTFUN1:def 6;

      ( dom b) = n by PARTFUN1:def 2;

      then ( rng SG) c= ( dom b) & ( rng S) c= ( dom b);

      then

       A18: ( dom (b * SG)) = ( dom SG) & ( dom (b * S)) = ( dom S) by RELAT_1: 27;

      

      then ((b * SG) /. Hi) = ((b * SG) . Hi) by A14, A7, PARTFUN1:def 6

      .= (b . (SG . Hi)) by A18, A14, A7, FUNCT_1: 12

      .= (b . ((SG * H) . i)) by A14, A13, FINSEQ_3: 25, A7, A10, FUNCT_1: 12

      .= ((b * S) . i) by A7, A18, A13, FINSEQ_3: 25, A10, FUNCT_1: 12

      .= ((b * S) /. i) by A7, A18, A13, FINSEQ_3: 25, A10, PARTFUN1:def 6;

      hence (yH /. i) = (( power L) . (((x * S) /. i),((b * S) /. i))) by A3, A17, A14, A15;

    end;

    theorem :: HILB10_2:20

    

     Th20: for O be Ordinal, L be well-unital commutative associative non trivial doubleLoopStr, x be Function of O, L, b be bag of O holds for perm be Permutation of O holds ( eval (b,x)) = ( eval ((b * perm),(x * perm)))

    proof

      let n be Ordinal, L be well-unital commutative associative non trivial doubleLoopStr, x be Function of n, L, b be bag of n;

      let perm be Permutation of n;

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

      consider y be FinSequence of L such that

       A1: ( len y) = ( len SG) & ( eval (b,x)) = ( Product y) and

       A2: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (( power L) . (((x * SG) /. i),((b * SG) /. i))) by POLYNOM2:def 2;

      

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

      

       A4: SG is one-to-one & ( len SG) = ( card ( support b)) by PRE_POLY: 10, PRE_POLY: 11, PRE_POLY: 82;

      

       A5: ( rng SG) = ( support b) by A3, PRE_POLY:def 2;

      set P = (perm " );

      

       A6: ( dom perm) = n = ( rng perm) & ( dom P) = n = ( rng P) by FUNCT_2: 52, FUNCT_2:def 3;

      

       A7: ( rng (P * SG)) c= ( support (b * perm))

      proof

        let y be object such that

         A8: y in ( rng (P * SG));

        consider w be object such that

         A9: w in ( dom (P * SG)) & ((P * SG) . w) = y by A8, FUNCT_1:def 3;

        

         A10: w in ( dom SG) & y = (P . (SG . w)) & (SG . w) in ( dom P) by A9, FUNCT_1: 11, FUNCT_1: 12;

        then

         A11: y in ( rng P) by FUNCT_1:def 3;

        

         A12: (SG . w) = (perm . y) by A10, FUNCT_1: 35, A6;

        (SG . w) in ( support b) by A5, A10, FUNCT_1:def 3;

        then

         A13: (b . (perm . y)) <> 0 by A12, PRE_POLY:def 7;

        (b . (perm . y)) = ((b * perm) . y) by A11, A6, FUNCT_1: 13;

        hence thesis by A13, PRE_POLY:def 7;

      end;

      

       A14: ( support (b * perm)) c= ( rng (P * SG))

      proof

        let x be object such that

         A15: x in ( support (b * perm));

        

         A16: ((b * perm) . x) <> 0 by A15, PRE_POLY:def 7;

        then x in ( dom (b * perm)) by FUNCT_1:def 2;

        then

         A17: x in ( dom perm) & (perm . x) in ( dom b) & ((b * perm) . x) = (b . (perm . x)) by FUNCT_1: 11, FUNCT_1: 12;

        then

         A18: x = (P . (perm . x)) & (perm . x) in ( support b) by A16, FUNCT_1: 34, PRE_POLY:def 7;

        then

        consider w be object such that

         A19: w in ( dom SG) & (SG . w) = (perm . x) by A5, FUNCT_1:def 3;

        w in ( dom (P * SG)) & ((P * SG) . w) = (P . (SG . w)) by A6, A17, A19, FUNCT_1: 11, FUNCT_1: 13;

        hence thesis by A18, A19, FUNCT_1:def 3;

      end;

      reconsider S = (P * SG) as one-to-one FinSequence of n by A4;

      consider Y be FinSequence of L such that

       A20: ( len Y) = ( card ( support (b * perm))) & ( eval ((b * perm),(x * perm))) = ( Product Y) and

       A21: for i be Nat st 1 <= i & i <= ( len Y) holds (Y /. i) = (( power L) . ((((x * perm) * S) /. i),(((b * perm) * S) /. i))) by Th19, A7, XBOOLE_0:def 10, A14;

      

       A22: ( len Y) = ( len y) by A20, A1, A4, Th2;

      for i be Nat st 1 <= i & i <= ( len Y) holds (Y . i) = (y . i)

      proof

        let i be Nat such that

         A23: 1 <= i <= ( len Y);

        

         A24: ( rng perm) = n by FUNCT_2:def 3;

        

         A25: n c= ( dom x) & n = ( dom b) by PARTFUN1:def 2;

        

         A26: ((x * perm) * S) = (((x * perm) * P) * SG) by RELAT_1: 36

        .= ((x * (perm * P)) * SG) by RELAT_1: 36

        .= ((x * ( id n)) * SG) by A24, FUNCT_1: 39

        .= (x * SG) by A25, RELAT_1: 51;

        

         A27: ((b * perm) * S) = (((b * perm) * P) * SG) by RELAT_1: 36

        .= ((b * (perm * P)) * SG) by RELAT_1: 36

        .= ((b * ( id n)) * SG) by A24, FUNCT_1: 39

        .= (b * SG) by A25, RELAT_1: 51;

        

         A28: i in ( dom y) & i in ( dom Y) by A22, A23, FINSEQ_3: 25;

        

        hence (Y . i) = (Y /. i) by PARTFUN1:def 6

        .= (( power L) . ((((x * perm) * S) /. i),(((b * perm) * S) /. i))) by A21, A23

        .= (y /. i) by A2, A23, A28, A22, A27, A26

        .= (y . i) by A28, PARTFUN1:def 6;

      end;

      hence thesis by A20, A1, A4, Th2, FINSEQ_1: 14;

    end;

    definition

      let O be Ordinal;

      let L be non empty ZeroStr;

      let s be Series of O, L;

      let perm be Permutation of O;

      :: HILB10_2:def4

      func s permuted_by perm -> Series of O, L means

      : Def4: for b be bag of O holds (it . b) = (s . (b * perm));

      existence

      proof

        defpred P[ Element of ( Bags O), Element of L] means $2 = (s . ($1 * perm));

        

         A1: for x be Element of ( Bags O) holds ex y be Element of L st P[x, y];

        consider f be Function of ( Bags O), L such that

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

        take f;

        let b be bag of O;

        b is Element of ( Bags O) by PRE_POLY:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let e1,e2 be Series of O, L such that

         A3: for b be bag of O holds (e1 . b) = (s . (b * perm)) and

         A4: for b be bag of O holds (e2 . b) = (s . (b * perm));

        now

          let b be Element of ( Bags O);

          (e1 . b) = (s . (b * perm)) = (e2 . b) by A3, A4;

          hence (e1 . b) = (e2 . b);

        end;

        hence thesis;

      end;

    end

    theorem :: HILB10_2:21

    

     Th21: for O be Ordinal, L be non empty ZeroStr, perm be Permutation of O, s be Series of O, L, b be bag of O holds b in ( Support (s permuted_by perm)) iff (b * perm) in ( Support s)

    proof

      let O be Ordinal, L be non empty ZeroStr, perm be Permutation of O, s be Series of O, L, b be bag of O;

      set P = (s permuted_by perm);

      

       A1: ( dom P) = ( Bags O) = ( dom s) by FUNCT_2:def 1;

      

       A2: (P . b) = (s . (b * perm)) by Def4;

      thus b in ( Support P) implies (b * perm) in ( Support s)

      proof

        assume b in ( Support P);

        then

         A3: (P . b) <> ( 0. L) by POLYNOM1:def 3;

        (b * perm) in ( Bags O) by PRE_POLY:def 12;

        hence thesis by A3, A1, A2, POLYNOM1:def 3;

      end;

      assume (b * perm) in ( Support s);

      then

       A4: (s . (b * perm)) <> ( 0. L) by POLYNOM1:def 3;

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

      hence thesis by A4, A1, A2, POLYNOM1:def 3;

    end;

    theorem :: HILB10_2:22

    

     Th22: for O be Ordinal, L be non empty ZeroStr, perm be Permutation of O, s be Series of O, L, b be bag of O holds (b * (perm " )) in ( Support (s permuted_by perm)) iff b in ( Support s)

    proof

      let O be Ordinal, L be non empty ZeroStr, perm be Permutation of O, s be Series of O, L, b be bag of O;

      set P = (s permuted_by perm);

      

       A1: ( dom P) = ( Bags O) = ( dom s) by FUNCT_2:def 1;

      

       A2: ( dom b) = O by PARTFUN1:def 2;

      ( dom perm) = O by FUNCT_2: 52;

      then ((perm " ) * perm) = ( id O) by FUNCT_1: 39;

      

      then ((b * (perm " )) * perm) = (b * ( id O)) by RELAT_1: 36

      .= b by A2, RELAT_1: 51;

      then

       A3: (P . (b * (perm " ))) = (s . b) by Def4;

      thus (b * (perm " )) in ( Support P) implies b in ( Support s)

      proof

        assume (b * (perm " )) in ( Support P);

        then

         A4: (P . (b * (perm " ))) <> ( 0. L) by POLYNOM1:def 3;

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

        hence thesis by A4, A1, A3, POLYNOM1:def 3;

      end;

      assume b in ( Support s);

      then

       A5: (s . b) <> ( 0. L) by POLYNOM1:def 3;

      (b * (perm " )) in ( Bags O) by PRE_POLY:def 12;

      hence thesis by A5, A1, A3, POLYNOM1:def 3;

    end;

    theorem :: HILB10_2:23

    

     Th23: for O be Ordinal, L be non empty ZeroStr, perm be Permutation of O, s be Series of O, L holds ( card ( Support s)) = ( card ( Support (s permuted_by perm)))

    proof

      let O be Ordinal, L be non empty ZeroStr, perm be Permutation of O, s be Series of O, L;

      set P = (s permuted_by perm);

      defpred R[ bag of O, bag of O] means $2 = ($1 * perm);

      

       A1: for x be Element of ( Bags O) holds ex y be Element of ( Bags O) st R[x, y]

      proof

        let x be Element of ( Bags O);

        (x * perm) in ( Bags O) by PRE_POLY:def 12;

        hence thesis;

      end;

      consider f be Function of ( Bags O), ( Bags O) such that

       A2: for x be Element of ( Bags O) holds R[x, (f . x)] from FUNCT_2:sch 3( A1);

      

       A3: ( dom f) = ( Bags O) by FUNCT_2: 52;

      ( rng perm) = O = ( dom perm) by FUNCT_2: 52, FUNCT_2:def 3;

      then

       A4: (perm * (perm " )) = ( id O) = ((perm " ) * perm) by FUNCT_1: 39;

      

       A5: f is one-to-one

      proof

        let x1,x2 be object such that

         A6: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        reconsider x1, x2 as Element of ( Bags O) by A6;

        

         A7: (f . x1) = (x1 * perm) & (f . x2) = (x2 * perm) by A2;

        

         A8: ( dom x1) = O = ( dom x2) by PARTFUN1:def 2;

        

         A9: ((x1 * perm) * (perm " )) = (x1 * ( id O)) by A4, RELAT_1: 36

        .= x1 by A8, RELAT_1: 51;

        ((x2 * perm) * (perm " )) = (x2 * ( id O)) by A4, RELAT_1: 36

        .= x2 by A8, RELAT_1: 51;

        hence thesis by A6, A7, A9;

      end;

      

       A10: (f .: ( Support P)) c= ( Support s)

      proof

        let y be object such that

         A11: y in (f .: ( Support P));

        consider x be object such that

         A12: x in ( dom f) & x in ( Support P) & (f . x) = y by A11, FUNCT_1:def 6;

        reconsider x as Element of ( Bags O) by A12;

        (f . x) = (x * perm) in ( Support s) by A2, Th21, A12;

        hence thesis by A12;

      end;

      ( Support s) c= (f .: ( Support P))

      proof

        let y be object such that

         A13: y in ( Support s);

        reconsider y as Element of ( Bags O) by A13;

        

         A14: (y * (perm " )) in ( Support P) by A13, Th22;

        

         A15: ( dom y) = O by PARTFUN1:def 2;

        (y * (perm " )) in ( Bags O) by PRE_POLY:def 12;

        

        then (f . (y * (perm " ))) = ((y * (perm " )) * perm) by A2

        .= (y * ( id O)) by A4, RELAT_1: 36

        .= y by A15, RELAT_1: 51;

        hence thesis by A3, FUNCT_1:def 6, A14;

      end;

      then (f .: ( Support P)) = ( Support s) by A10, XBOOLE_0:def 10;

      hence thesis by CARD_1: 5, A5, A3, CARD_1: 33;

    end;

    theorem :: HILB10_2:24

    

     Th24: for O be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of O, L, x be Function of O, L holds for S be one-to-one FinSequence of ( Bags O) st ( rng S) = ( Support p) holds ex y be FinSequence of L st ( len y) = ( card ( Support p)) & ( eval (p,x)) = ( Sum y) & for i be Nat st 1 <= i & i <= ( len y) holds (y /. i) = (((p * S) /. i) * ( eval ((S /. i),x)))

    proof

      let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L, x be Function of n, L;

      let S be one-to-one FinSequence of ( Bags n) such that

       A1: ( rng S) = ( Support p);

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

      consider y be FinSequence of L such that

       A2: ( len y) = ( len SG) & ( eval (p,x)) = ( Sum y) and

       A3: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((p * SG) /. i) * ( eval ((SG /. i),x))) by POLYNOM2:def 4;

      

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

      

       A5: SG is one-to-one & ( len SG) = ( card ( Support p)) by POLYNOM2: 18, PRE_POLY: 10, PRE_POLY: 11;

      

       A6: ( rng SG) = ( Support p) by A4, PRE_POLY:def 2;

      then

      consider H be Function such that

       A7: ( dom H) = ( dom S) & ( rng H) = ( dom SG) & H is one-to-one & (SG * H) = S by A1, A5, RFINSEQ: 26, CLASSES1: 77;

      

       A8: ( len S) = ( len SG) by A1, A5, A6, FINSEQ_1: 48;

      

       A9: ( dom y) = ( dom SG) = ( dom S) by A2, A8, FINSEQ_3: 29;

      then

       A10: ( dom (y * H)) = ( dom H) & ( dom S) = ( Seg ( len S)) by A7, RELAT_1: 27, FINSEQ_1:def 3;

      then

      reconsider yH = (y * H) as FinSequence by A7, FINSEQ_1:def 2;

      reconsider H as Function of ( dom y), ( dom y) by A7, A9, FUNCT_2: 1;

      H is onto by A7, A2, FINSEQ_3: 29;

      then

      reconsider H as Permutation of ( dom y) by A7;

      

       A11: ( rng y) c= the carrier of L;

      ( rng yH) c= ( rng y) by RELAT_1: 26;

      then ( rng yH) c= the carrier of L by A11;

      then

      reconsider yH as FinSequence of L by FINSEQ_1:def 4;

      reconsider yH as FinSequence of L;

      take yH;

      thus ( len yH) = ( card ( Support p)) by A7, A10, FINSEQ_3: 29, A8, A5;

      

       A12: ( len y) = ( len yH) by A2, A8, A7, A10, FINSEQ_3: 29;

      for i be Nat st i in ( dom yH) holds (yH . i) = (y . (H . i)) by FUNCT_1: 12;

      hence ( eval (p,x)) = ( Sum yH) by A2, A12, RLVECT_2: 6;

      let i be Nat such that

       A13: 1 <= i <= ( len yH);

      set Hi = (H /. i);

      i in ( dom yH) by A13, FINSEQ_3: 25;

      then

       A14: (yH /. i) = (yH . i) & (H . i) = Hi & (yH . i) = (y . (H . i)) & (H . i) in ( rng H) by A10, PARTFUN1:def 6, FUNCT_1: 12, FUNCT_1:def 3;

      then

       A15: 1 <= Hi <= ( len y) & Hi in NAT & (y . Hi) = (y /. Hi) by FINSEQ_3: 25, PARTFUN1:def 6;

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

      then ( rng SG) c= ( dom p) & ( rng S) c= ( dom p);

      then

       A16: ( dom (p * SG)) = ( dom SG) & ( dom (p * S)) = ( dom S) by RELAT_1: 27;

      

      then

       A17: ((p * SG) /. Hi) = ((p * SG) . Hi) by A14, A7, PARTFUN1:def 6

      .= (p . (SG . Hi)) by A16, A14, A7, FUNCT_1: 12

      .= (p . ((SG * H) . i)) by A14, A13, FINSEQ_3: 25, A7, A10, FUNCT_1: 12

      .= ((p * S) . i) by A7, A16, A13, FINSEQ_3: 25, A10, FUNCT_1: 12

      .= ((p * S) /. i) by A7, A16, A13, FINSEQ_3: 25, A10, PARTFUN1:def 6;

      (SG /. Hi) = (SG . (H . i)) by A14, A7, PARTFUN1:def 6

      .= ((SG * H) . i) by A13, FINSEQ_3: 25, A7, A10, FUNCT_1: 12

      .= (S /. i) by A13, FINSEQ_3: 25, A7, A10, PARTFUN1:def 6;

      hence (yH /. i) = (((p * S) /. i) * ( eval ((S /. i),x))) by A3, A17, A14, A15;

    end;

    registration

      let O be Ordinal;

      let L be non empty ZeroStr;

      let perm be Permutation of O;

      let p be Polynomial of O, L;

      cluster (p permuted_by perm) -> finite-Support;

      coherence

      proof

        

         A1: ( Support p) is finite by POLYNOM1:def 5;

        ( card ( Support p)) = ( card ( Support (p permuted_by perm))) by Th23;

        then ( Support (p permuted_by perm)) is finite by A1;

        hence thesis by POLYNOM1:def 5;

      end;

    end

    theorem :: HILB10_2:25

    

     Th25: for O be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive commutative associative non trivial doubleLoopStr, p be Polynomial of O, L, x be Function of O, L holds for perm be Permutation of O holds ( eval (p,x)) = ( eval ((p permuted_by perm),(x * (perm " ))))

    proof

      let O be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive commutative associative non trivial doubleLoopStr, p be Polynomial of O, L, x be Function of O, L;

      let perm be Permutation of O;

      set SB = ( SgmX (( BagOrder O),( Support p)));

      consider y be FinSequence of L such that

       A1: ( len y) = ( len SB) & ( eval (p,x)) = ( Sum y) and

       A2: for i be Element of NAT st 1 <= i & i <= ( len y) holds (y /. i) = (((p * SB) /. i) * ( eval ((SB /. i),x))) by POLYNOM2:def 4;

      

       A3: ( BagOrder O) linearly_orders ( Support p) by POLYNOM2: 18;

      

       A4: SB is one-to-one & ( len SB) = ( card ( Support p)) by PRE_POLY: 10, PRE_POLY: 11, POLYNOM2: 18;

      

       A5: ( rng SB) = ( Support p) by A3, PRE_POLY:def 2;

      set P = (p permuted_by perm);

      defpred R[ bag of O, bag of O] means $2 = ($1 * (perm " ));

      

       A6: for x be Element of ( Bags O) holds ex y be Element of ( Bags O) st R[x, y]

      proof

        let x be Element of ( Bags O);

        (x * (perm " )) in ( Bags O) by PRE_POLY:def 12;

        hence thesis;

      end;

      consider f be Function of ( Bags O), ( Bags O) such that

       A7: for x be Element of ( Bags O) holds R[x, (f . x)] from FUNCT_2:sch 3( A6);

      

       A8: ( dom f) = ( Bags O) by FUNCT_2: 52;

      ( rng perm) = O = ( dom perm) by FUNCT_2: 52, FUNCT_2:def 3;

      then

       A9: (perm * (perm " )) = ( id O) = ((perm " ) * perm) by FUNCT_1: 39;

      

       A10: f is one-to-one

      proof

        let x1,x2 be object such that

         A11: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        reconsider x1, x2 as Element of ( Bags O) by A11;

        

         A12: (f . x1) = (x1 * (perm " )) & (f . x2) = (x2 * (perm " )) by A7;

        

         A13: ( dom x1) = O = ( dom x2) by PARTFUN1:def 2;

        

         A14: ((x1 * (perm " )) * perm) = (x1 * ( id O)) by A9, RELAT_1: 36

        .= x1 by A13, RELAT_1: 51;

        ((x2 * (perm " )) * perm) = (x2 * ( id O)) by A9, RELAT_1: 36

        .= x2 by A13, RELAT_1: 51;

        hence thesis by A11, A12, A14;

      end;

      reconsider fSB = (f * SB) as one-to-one FinSequence of ( Bags O) by A4, A10;

      ( rng SB) c= ( dom f) by A8;

      then

       A15: ( dom fSB) = ( dom SB) by RELAT_1: 27;

      

       A16: ( rng fSB) c= ( Support P)

      proof

        let y be object such that

         A17: y in ( rng fSB);

        consider x be object such that

         A18: x in ( dom fSB) & (fSB . x) = y by FUNCT_1:def 3, A17;

        

         A19: y = (f . (SB . x)) & x in ( dom SB) & (SB . x) in ( dom f) by A18, FUNCT_1: 11, FUNCT_1: 12;

        then

        reconsider SBx = (SB . x) as Element of ( Bags O);

        SBx in ( Support p) by A19, A5, FUNCT_1:def 3;

        then (SBx * (perm " )) in ( Support P) by Th22;

        hence thesis by A7, A19;

      end;

      ( Support P) c= ( rng fSB)

      proof

        let y be object such that

         A20: y in ( Support P);

        reconsider y as Element of ( Bags O) by A20;

        

         A21: ( dom y) = O by PARTFUN1:def 2;

        

         A22: (y * perm) in ( Support p) by A20, Th21;

        

        then

         A23: (f . (y * perm)) = ((y * perm) * (perm " )) by A7

        .= (y * ( id O)) by A9, RELAT_1: 36

        .= y by A21, RELAT_1: 51;

        consider w be object such that

         A24: w in ( dom SB) & (SB . w) = (y * perm) by A5, A22, FUNCT_1:def 3;

        w in ( dom fSB) & (fSB . w) = y by A8, A22, A23, A24, FUNCT_1: 11, FUNCT_1: 13;

        hence thesis by FUNCT_1:def 3;

      end;

      then

      consider z be FinSequence of L such that

       A25: ( len z) = ( card ( Support P)) & ( eval (P,(x * (perm " )))) = ( Sum z) and

       A26: for i be Nat st 1 <= i & i <= ( len z) holds (z /. i) = (((P * fSB) /. i) * ( eval ((fSB /. i),(x * (perm " ))))) by A16, XBOOLE_0:def 10, Th24;

      

       A27: ( len y) = ( len z) by A1, A4, A25, Th23;

      for i be Nat st 1 <= i <= ( len y) holds (y . i) = (z . i)

      proof

        let i be Nat such that

         A28: 1 <= i <= ( len y);

        

         A29: i in NAT by ORDINAL1:def 12;

        

         A30: i in ( dom y) & i in ( dom z) & i in ( dom SB) by A28, A1, FINSEQ_3: 25, A27;

        then

         A31: (SB . i) = (SB /. i) by PARTFUN1:def 6;

        then

        reconsider SBi = (SB . i) as Element of ( Bags O);

        

         A32: ( dom SBi) = O by PARTFUN1:def 2;

        

         A33: ((SBi * (perm " )) * perm) = (SBi * ( id O)) by A9, RELAT_1: 36

        .= SBi by A32, RELAT_1: 51;

        ( dom p) = ( Bags O) = ( dom P) by FUNCT_2:def 1;

        then ( rng SB) c= ( dom p) & ( rng fSB) c= ( dom P);

        then

         A34: ( dom (p * SB)) = ( dom SB) & ( dom (P * fSB)) = ( dom fSB) by RELAT_1: 27;

        

        then

         A35: ((P * fSB) /. i) = ((P * fSB) . i) by A15, A28, FINSEQ_3: 25, A1, PARTFUN1:def 6

        .= (P . (fSB . i)) by A1, A15, A28, FINSEQ_3: 25, A34, FUNCT_1: 12

        .= (P . (f . SBi)) by A15, A28, FINSEQ_3: 25, A1, FUNCT_1: 12

        .= (P . (SBi * (perm " ))) by A7

        .= (p . ((SBi * (perm " )) * perm)) by Def4

        .= ((p * SB) . i) by A28, A1, A33, FINSEQ_3: 25, A34, FUNCT_1: 12

        .= ((p * SB) /. i) by A34, A28, A1, FINSEQ_3: 25, PARTFUN1:def 6;

        

         A36: ((SB /. i) * (perm " )) = (f . SBi) by A7, A31

        .= (fSB . i) by A15, A28, A1, FINSEQ_3: 25, FUNCT_1: 12

        .= (fSB /. i) by A15, A28, A1, FINSEQ_3: 25, PARTFUN1:def 6;

        

        thus (y . i) = (y /. i) by A30, PARTFUN1:def 6

        .= (((p * SB) /. i) * ( eval ((SB /. i),x))) by A29, A2, A28

        .= (((P * fSB) /. i) * ( eval ((fSB /. i),(x * (perm " ))))) by A35, A36, Th20

        .= (z /. i) by A26, A28, A27

        .= (z . i) by A30, PARTFUN1:def 6;

      end;

      hence thesis by FINSEQ_1: 14, A1, A4, A25, Th23;

    end;

    theorem :: HILB10_2:26

    

     Th26: for O be Ordinal, L be non empty ZeroStr, s be Series of O, L, perm be Permutation of O holds ( rng (s permuted_by perm)) = ( rng s)

    proof

      let O be Ordinal, L be non empty ZeroStr, s be Series of O, L, perm be Permutation of O;

      set P = (s permuted_by perm);

      

       A1: ( dom P) = ( Bags O) & ( dom s) = ( Bags O) by FUNCT_2:def 1;

      thus ( rng P) c= ( rng s)

      proof

        let y be object;

        assume y in ( rng P);

        then

        consider x be object such that

         A2: x in ( dom P) & (P . x) = y by FUNCT_1:def 3;

        reconsider x as Element of ( Bags O) by A2;

        

         A3: (x * perm) in ( dom s) by A1, PRE_POLY:def 12;

        (s . (x * perm)) = (P . x) by Def4;

        hence thesis by A3, FUNCT_1:def 3, A2;

      end;

      let y be object;

      assume y in ( rng s);

      then

      consider x be object such that

       A4: x in ( dom s) & (s . x) = y by FUNCT_1:def 3;

      reconsider x as Element of ( Bags O) by A4;

      

       A5: ( dom x) = O by PARTFUN1:def 2;

      ( dom perm) = O by FUNCT_2: 52;

      then ((perm " ) * perm) = ( id O) by FUNCT_1: 39;

      

      then ((x * (perm " )) * perm) = (x * ( id O)) by RELAT_1: 36

      .= x by A5, RELAT_1: 51;

      then

       A6: (P . (x * (perm " ))) = (s . x) by Def4;

      (x * (perm " )) in ( dom P) by A1, PRE_POLY:def 12;

      hence thesis by A4, A6, FUNCT_1:def 3;

    end;

    begin

    theorem :: HILB10_2:27

    

     Th27: for L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L holds ex q be Polynomial of (n + m), L st ( rng q) c= (( rng p) \/ {( 0. L)}) & for x be Function of n, L, y be Function of (n + m), L st (y | n) = x holds ( eval (p,x)) = ( eval (q,y))

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n, L;

      defpred P[ Nat] means ex q be Polynomial of (n + $1), L st ( rng q) c= (( rng p) \/ {( 0. L)}) & for x be Function of n, L, y be Function of (n + $1), L st (y | n) = x holds ( eval (p,x)) = ( eval (q,y));

      

       A1: P[ 0 ]

      proof

        reconsider q = p as Polynomial of (n + 0 ), L;

        take q;

        thus ( rng q) c= (( rng p) \/ {( 0. L)}) by XBOOLE_1: 7;

        thus thesis;

      end;

      

       A2: P[k] implies P[(k + 1)]

      proof

        set k1 = (k + 1);

        assume P[k];

        then

        consider q be Polynomial of (n + k), L such that

         A3: ( rng q) c= (( rng p) \/ {( 0. L)}) and

         A4: for x be Function of n, L, y be Function of (n + k), L st (y | n) = x holds ( eval (p,x)) = ( eval (q,y));

        reconsider P = (q extended_by_0 ) as Polynomial of (n + k1), L;

        take P;

        ( rng P) = (( rng q) \/ {( 0. L)}) by Th10;

        then ( rng P) c= ((( rng p) \/ {( 0. L)}) \/ {( 0. L)}) by A3, XBOOLE_1: 13;

        hence ( rng P) c= (( rng p) \/ {( 0. L)}) by XBOOLE_1: 7, XBOOLE_1: 12;

        let x be Function of n, L, y be Function of (n + k1), L such that

         A5: (y | n) = x;

        

         A6: ( rng (y | (n + k))) c= ( rng y) & ( rng y) c= the carrier of L by RELAT_1: 70;

        ( len ( @ y)) = (n + k1) & (n + k) < ((n + k) + 1) by CARD_1:def 7, NAT_1: 13;

        then ( len (( @ y) | (n + k))) = (n + k) by AFINSQ_1: 54;

        then

        reconsider Y = (( @ y) | (n + k)) as Function of (n + k), L by A6, FUNCT_2: 2;

        ( Segm n) c= ( Segm (n + k)) by NAT_1: 39, NAT_1: 11;

        then

         A7: (Y | n) = x by A5, RELAT_1: 74;

        

        thus ( eval (P,y)) = ( eval (q,Y)) by Th18

        .= ( eval (p,x)) by A4, A7;

      end;

       P[k] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: HILB10_2:28

    

     Th28: for L be Abelian right_zeroed add-associative right_complementable well-unital distributive commutative associative non trivial doubleLoopStr, p be Polynomial of (n + m), L holds ex q be Polynomial of ((n + k) + m), L st ( rng q) c= (( rng p) \/ {( 0. L)}) & for XY be Function of (n + m), L, XanyY be Function of ((n + k) + m), L st (XY | n) = (XanyY | n) & (( @ XY) /^ n) = (( @ XanyY) /^ (n + k)) holds ( eval (p,XY)) = ( eval (q,XanyY))

    proof

      let L be Abelian right_zeroed add-associative right_complementable well-unital distributive commutative associative non trivial doubleLoopStr, p be Polynomial of (n + m), L;

      consider P be Polynomial of ((n + m) + k), L such that

       A1: ( rng P) c= (( rng p) \/ {( 0. L)}) and

       A2: for x be Function of (n + m), L, y be Function of ((n + m) + k), L st (y | (n + m)) = x holds ( eval (p,x)) = ( eval (P,y)) by Th27;

      reconsider P1 = P as Polynomial of ((n + k) + m), L;

      set I = ( id ((n + k) + m));

      ( dom I) = ((n + k) + m);

      then

      reconsider I as XFinSequence by AFINSQ_1: 5;

      set nm = (n + m), Inm = (I | nm);

      

       A3: I = (Inm ^ (I /^ nm));

      

       A4: Inm = ((Inm | n) ^ (Inm /^ n));

      

       A5: ( rng I) = (( rng Inm) \/ ( rng (I /^ nm))) by A3, AFINSQ_1: 26;

      

       A6: ( rng Inm) misses ( rng (I /^ nm)) by A3, Th1;

      

       A7: ( rng Inm) = (( rng (Inm | n)) \/ ( rng (Inm /^ n))) by A4, AFINSQ_1: 26;

      

       A8: ( rng (Inm | n)) misses ( rng (Inm /^ n)) by A4, Th1;

      ( rng (Inm | n)) misses ( rng (I /^ nm)) by A6, XBOOLE_1: 63, A7, XBOOLE_1: 7;

      then

       A9: ((Inm | n) ^ (I /^ nm)) is one-to-one by CARD_FIN: 52;

      

       A10: ( rng ((Inm | n) ^ (I /^ nm))) = (( rng (Inm | n)) \/ ( rng (I /^ nm))) by AFINSQ_1: 26;

      ( rng (I /^ nm)) misses ( rng (Inm /^ n)) by A6, XBOOLE_1: 63, A7, XBOOLE_1: 7;

      then ( rng ((Inm | n) ^ (I /^ nm))) misses ( rng (Inm /^ n)) by A10, A8, XBOOLE_1: 70;

      then

       A11: (((Inm | n) ^ (I /^ nm)) ^ (Inm /^ n)) is one-to-one by A9, CARD_FIN: 52;

      

       A12: ( rng (((Inm | n) ^ (I /^ nm)) ^ (Inm /^ n))) = (( rng ((Inm | n) ^ (I /^ nm))) \/ ( rng (Inm /^ n))) by AFINSQ_1: 26

      .= ((( rng (Inm | n)) \/ ( rng (I /^ nm))) \/ ( rng (Inm /^ n))) by AFINSQ_1: 26

      .= ((n + k) + m) by A5, A7, XBOOLE_1: 4;

      ( len (((Inm | n) ^ (I /^ nm)) ^ (Inm /^ n))) = (( len ((Inm | n) ^ (I /^ nm))) + ( len (Inm /^ n))) by AFINSQ_1: 17

      .= ((( len (Inm | n)) + ( len (I /^ nm))) + ( len (Inm /^ n))) by AFINSQ_1: 17

      .= ((( len (Inm | n)) + ( len (Inm /^ n))) + ( len (I /^ nm)))

      .= (( len Inm) + ( len (I /^ nm))) by A4, AFINSQ_1: 17

      .= ( len I) by A3, AFINSQ_1: 17;

      then

      reconsider III = (((Inm | n) ^ (I /^ nm)) ^ (Inm /^ n)) as Function of ((n + k) + m), ((n + k) + m) by A12, FUNCT_2: 1;

      III is onto by A12;

      then

      reconsider III as Permutation of ((n + k) + m) by A11;

      take T = (P1 permuted_by (III " ));

      thus ( rng T) c= (( rng p) \/ {( 0. L)}) by A1, Th26;

      let XY be Function of (n + m), L, XanyY be Function of ((n + k) + m), L such that

       A13: (XY | n) = (XanyY | n) & (( @ XY) /^ n) = (( @ XanyY) /^ (n + k));

      

       A14: ( len ( @ XY)) = (n + m) & ( len ( @ XanyY)) = ((n + k) + m) by FUNCT_2:def 1;

      

      then

       A15: ( len (( @ XY) /^ n)) = ((n + m) -' n) by AFINSQ_2:def 2

      .= m by NAT_D: 34;

      

       A16: ( len (( @ XanyY) /^ (n + k))) = (((n + k) + m) -' (n + k)) by A14, AFINSQ_2:def 2

      .= m by NAT_D: 34;

      ( len (( @ XanyY) | (n + k))) = (n + k) by A14, AFINSQ_1: 54, NAT_1: 11;

      

      then

       A17: ( len ((( @ XanyY) | (n + k)) /^ n)) = ((n + k) -' n) by AFINSQ_2:def 2

      .= k by NAT_D: 34;

      then

       A18: ( len (( @ XY) ^ ((( @ XanyY) | (n + k)) /^ n))) = ((n + m) + k) by A14, AFINSQ_1: 17;

      ( rng (( @ XY) ^ ((( @ XanyY) | (n + k)) /^ n))) c= the carrier of L by RELAT_1:def 19;

      then

      reconsider R = (( @ XY) ^ ((( @ XanyY) | (n + k)) /^ n)) as Function of ((n + m) + k), L by A18, FUNCT_2: 2;

      reconsider r = R as Function of ((n + k) + m), L;

      (R | (n + m)) = (( @ XY) | (n + m)) by AFINSQ_1: 58, A14

      .= ( @ XY);

      then

       A19: ( eval (p,XY)) = ( eval (P,R)) by A2;

      ((III " ) " ) = III by FUNCT_1: 43;

      then

       A20: ( eval (P1,r)) = ( eval (T,(r * III))) by Th25;

      

       A21: ( dom ( @ (r * III))) = ((n + k) + m) = ( dom ( @ XanyY)) by FUNCT_2:def 1;

      (n + m) <= ((n + m) + k) by NAT_1: 11;

      then nm <= ( len I);

      then

       A22: ( len Inm) = nm & ( len (I /^ nm)) = ((nm + k) -' nm) by AFINSQ_1: 54, AFINSQ_2:def 2;

      then

       A23: ( len (I /^ nm)) = k by NAT_D: 34;

      

       A24: n <= nm by NAT_1: 11;

      

       A25: ( len (Inm | n)) = n & ( len (Inm /^ n)) = (nm -' n) by A22, NAT_1: 11, AFINSQ_1: 54, AFINSQ_2:def 2;

      then

       A26: ( len (Inm /^ n)) = m by NAT_D: 34;

      

       A27: ( len ((Inm | n) ^ (I /^ nm))) = (n + k) by A23, A25, AFINSQ_1: 17;

      for k st k in ( dom ( @ XanyY)) holds (( @ (r * III)) . k) = (( @ XanyY) . k)

      proof

        let w be Nat;

        assume

         A28: w in ( dom ( @ XanyY));

        per cases ;

          suppose

           A29: w < n;

          then

           A30: w in ( dom (Inm | n)) c= ( dom ((Inm | n) ^ (I /^ nm))) by A25, AFINSQ_1: 66, AFINSQ_1: 21;

          w < nm by A29, A24, XXREAL_0: 2;

          then

           A31: w in ( Segm nm) by NAT_1: 44;

          

           A32: (III . w) = (((Inm | n) ^ (I /^ nm)) . w) by AFINSQ_1:def 3, A30

          .= ((Inm | n) . w) by A30, AFINSQ_1:def 3

          .= (Inm . w) by A29, A25, AFINSQ_1: 66, FUNCT_1: 47

          .= (I . w) by A31, FUNCT_1: 49

          .= w by A21, A28, FUNCT_1: 17;

          (w + 0 ) < (n + m) by A29, XREAL_1: 8;

          then w in ( dom ( @ XY)) by A14, AFINSQ_1: 66;

          

          then (r . w) = (( @ XY) . w) by AFINSQ_1:def 3

          .= ((( @ XY) | n) . w) by A29, A25, AFINSQ_1: 66, FUNCT_1: 49

          .= (XanyY . w) by A13, A29, A25, AFINSQ_1: 66, FUNCT_1: 49;

          hence thesis by A32, A28, FUNCT_1: 12, A21;

        end;

          suppose

           A33: (n + k) > w >= n;

          then

          reconsider wn = (w - n) as Nat by NAT_1: 21;

          (n + k) > (n + wn) by A33;

          then

           A34: wn in ( Segm k) by NAT_1: 44, XREAL_1: 6;

          

           A35: w in ( Segm (n + k)) by A33, NAT_1: 44;

          (nm + wn) = (m + w);

          then (nm + wn) < (m + (n + k)) by A33, XREAL_1: 6;

          then

           A36: (nm + wn) in ( Segm ((n + m) + k)) by NAT_1: 44;

          w in ( dom ((Inm | n) ^ (I /^ nm))) by A33, A27, AFINSQ_1: 66;

          

          then

           A37: (III . w) = (((Inm | n) ^ (I /^ nm)) . w) by AFINSQ_1:def 3

          .= ((I /^ nm) . wn) by A33, AFINSQ_1: 18, A23, A25

          .= (I . (nm + wn)) by A23, A34, AFINSQ_2:def 2

          .= (nm + wn) by A36, FUNCT_1: 17;

          (r . (nm + wn)) = (((( @ XanyY) | (n + k)) /^ n) . wn) by A14, A17, A34, AFINSQ_1:def 3

          .= ((( @ XanyY) | (n + k)) . (wn + n)) by A17, A34, AFINSQ_2:def 2

          .= (( @ XanyY) . w) by A35, FUNCT_1: 49;

          hence thesis by A37, A28, FUNCT_1: 12, A21;

        end;

          suppose w >= (n + k);

          then

          reconsider wnk = (w - (n + k)) as Nat by NAT_1: 21;

          

           A38: ((n + k) + m) > ((n + k) + wnk) by A28, A14, AFINSQ_1: 66;

          then

           A39: m > wnk by XREAL_1: 6;

          

           A40: wnk in ( Segm m) by NAT_1: 44, A38, XREAL_1: 6;

          then

           A41: wnk in ( dom (Inm /^ n)) by A25, NAT_D: 34;

          (wnk + n) < (m + n) by A39, XREAL_1: 6;

          then ((wnk + n) + 0 ) < ((m + n) + k) by XREAL_1: 8;

          then

           A42: (wnk + n) in ( Segm ((n + k) + m)) & (wnk + n) in ( Segm (m + n)) by A39, XREAL_1: 6, NAT_1: 44;

          

           A43: (III . ((n + k) + wnk)) = ((Inm /^ n) . wnk) by A40, A26, A27, AFINSQ_1:def 3

          .= (Inm . (n + wnk)) by A41, AFINSQ_2:def 2

          .= (I . (n + wnk)) by A42, FUNCT_1: 49

          .= (n + wnk) by A42, FUNCT_1: 17;

          (r . (n + wnk)) = (( @ XY) . (n + wnk)) by A14, A42, AFINSQ_1:def 3

          .= ((( @ XY) /^ n) . wnk) by A40, A15, AFINSQ_2:def 2

          .= (( @ XanyY) . ((n + k) + wnk)) by A13, A16, A40, AFINSQ_2:def 2;

          hence thesis by A43, A28, FUNCT_1: 12, A21;

        end;

      end;

      hence thesis by A20, A19, A21, AFINSQ_1: 8;

    end;

    begin

    reserve x,s for object;

    definition

      let D be non empty set;

      let n be Nat;

      :: HILB10_2:def5

      func n -xtuples_of D -> Subset of (D ^omega ) means

      : Def5: x in it iff x is n -element XFinSequence of D;

      existence

      proof

        take X = the set of all x where x be n -element XFinSequence of D;

        X c= (D ^omega )

        proof

          let y be object;

          assume y in X;

          then ex x be n -element XFinSequence of D st y = x;

          hence thesis by AFINSQ_1:def 7;

        end;

        hence X is Subset of (D ^omega );

        let x;

        thus x in X implies x is n -element XFinSequence of D

        proof

          assume x in X;

          then ex y be n -element XFinSequence of D st x = y;

          hence thesis;

        end;

        assume x is n -element XFinSequence of D;

        hence thesis;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of (D ^omega ) such that

         A1: x in X1 iff x is n -element XFinSequence of D and

         A2: x in X2 iff x is n -element XFinSequence of D;

        now

          let x;

          x in X1 iff x is n -element XFinSequence of D by A1;

          hence x in X1 iff x in X2 by A2;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let D be non empty set;

      let n be Nat;

      cluster (n -xtuples_of D) -> non empty;

      coherence

      proof

         the n -element XFinSequence of D in (n -xtuples_of D) by Def5;

        hence thesis;

      end;

      cluster -> n -elementD -valued for Element of (n -xtuples_of D);

      coherence by Def5;

    end

    definition

      let n be Nat;

      let A be Subset of (n -xtuples_of NAT );

      :: HILB10_2:def6

      attr A is diophantine means

      : Def6: ex m be Nat, p be INT -valued Polynomial of (n + m), F_Real st for s 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 ;

    end

    registration

      let n be Nat;

      cluster empty -> diophantine for Subset of (n -xtuples_of NAT );

      coherence

      proof

        let A be Subset of (n -xtuples_of NAT );

        assume

         A1: A is empty;

        reconsider p = ( 1_ ((n + 0 ), F_Real )) as INT -valued Polynomial of (n + 0 ), F_Real ;

        take 0 , p;

        let s;

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

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

         A2: s = x & ( eval (p,( @ (x ^ y)))) = 0 ;

        ( eval (p,( @ (x ^ y)))) = ( 1. F_Real ) by POLYNOM2: 21

        .= 1;

        hence thesis by A2;

      end;

      cluster ( [#] (n -xtuples_of NAT )) -> diophantine;

      coherence

      proof

        reconsider p = ( 0_ ((n + 0 ), F_Real )) as INT -valued Polynomial of (n + 0 ), F_Real ;

        set ALL = ( [#] (n -xtuples_of NAT ));

        take 0 , p;

        let s;

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

        proof

          assume s in ALL;

          then

          reconsider x = s as n -element NAT -valued XFinSequence;

          set y = the 0 -element XFinSequence of NAT ;

          ( eval (p,( @ (x ^ y)))) = ( 0. F_Real ) by POLYNOM2: 20

          .= 0 ;

          hence thesis;

        end;

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

         A3: s = x & ( eval (p,( @ (x ^ y)))) = 0 ;

        thus thesis by A3, Def5;

      end;

    end

    registration

      let n be zero Nat;

      cluster -> diophantine for Subset of (n -xtuples_of NAT );

      coherence

      proof

        let S be Subset of (n -xtuples_of NAT );

        per cases ;

          suppose S = {} ;

          hence thesis;

        end;

          suppose S <> 0 ;

          then

          consider x such that

           A1: x in S by XBOOLE_0:def 1;

          reconsider x as n -element XFinSequence of NAT by A1;

          (n -xtuples_of NAT ) c= S by A1;

          then ( [#] (n -xtuples_of NAT )) = S by XBOOLE_0:def 10;

          hence thesis;

        end;

      end;

    end

    registration

      let n be Nat;

      cluster non empty diophantine for Subset of (n -xtuples_of NAT );

      existence

      proof

        take ( [#] (n -xtuples_of NAT ));

        thus thesis;

      end;

      cluster empty diophantine for Subset of (n -xtuples_of NAT );

      existence

      proof

        take ( {} (n -xtuples_of NAT ));

        thus thesis;

      end;

    end

    registration

      let n be Nat;

      let A,B be diophantine Subset of (n -xtuples_of NAT );

      cluster (A /\ B) -> diophantine;

      coherence

      proof

        consider nA be Nat, pA be INT -valued Polynomial of (n + nA), F_Real such that

         A1: for s holds s in A iff ex x be n -element XFinSequence of NAT , y be nA -element XFinSequence of NAT st s = x & ( eval (pA,( @ (x ^ y)))) = 0 by Def6;

        consider nB be Nat, pB be INT -valued Polynomial of (n + nB), F_Real such that

         A2: for s holds s in B iff ex x be n -element XFinSequence of NAT , y be nB -element XFinSequence of NAT st s = x & ( eval (pB,( @ (x ^ y)))) = 0 by Def6;

        (A /\ B) is diophantine

        proof

          take N = (nA + nB);

          consider qA be Polynomial of ((n + nA) + nB), F_Real such that

           A3: ( rng qA) c= (( rng pA) \/ {( 0. F_Real )}) and

           A4: for x be Function of (n + nA), F_Real , y be Function of ((n + nA) + nB), F_Real st (y | (n + nA)) = x holds ( eval (pA,x)) = ( eval (qA,y)) by Th27;

          ( rng qA) c= INT by A3, INT_1:def 2;

          then

          reconsider qA as INT -valued Polynomial of (n + N), F_Real by RELAT_1:def 19;

          consider qB be Polynomial of ((n + nA) + nB), F_Real such that

           A5: ( rng qB) c= (( rng pB) \/ {( 0. F_Real )}) and

           A6: for XY be Function of (n + nB), F_Real , XanyY be Function of ((n + nA) + nB), F_Real st (XY | n) = (XanyY | n) & (( @ XY) /^ n) = (( @ XanyY) /^ (n + nA)) holds ( eval (pB,XY)) = ( eval (qB,XanyY)) by Th28;

          ( rng qB) c= INT by A5, INT_1:def 2;

          then

          reconsider qB as INT -valued Polynomial of (n + N), F_Real by RELAT_1:def 19;

          take Q = ((qA *' qA) + (qB *' qB));

          let y be object;

          thus y in (A /\ B) implies ex x be n -element XFinSequence of NAT , y1 be N -element XFinSequence of NAT st y = x & ( eval (Q,( @ (x ^ y1)))) = 0

          proof

            assume

             A7: y in (A /\ B);

            then y in A by XBOOLE_0:def 4;

            then

            consider xA be n -element XFinSequence of NAT , yA be nA -element XFinSequence of NAT such that

             A8: y = xA & ( eval (pA,( @ (xA ^ yA)))) = 0 by A1;

            y in B by A7, XBOOLE_0:def 4;

            then

            consider xB be n -element XFinSequence of NAT , yB be nB -element XFinSequence of NAT such that

             A9: y = xB & ( eval (pB,( @ (xB ^ yB)))) = 0 by A2;

            reconsider X = ( @ ((xA ^ yA) ^ yB)) as Function of (n + N), F_Real ;

            

             A10: ( len (xA ^ yA)) = (n + nA) by CARD_1:def 7;

            then (((xA ^ yA) ^ yB) | (n + nA)) = (xA ^ yA) by AFINSQ_1: 57;

            then

             A11: ( eval (qA,X)) = 0 by A8, A4;

            

             A12: X = (xA ^ (yA ^ yB)) by AFINSQ_1: 27;

            

             A13: ( len xA) = n by CARD_1:def 7;

            then

             A14: (( @ ( @ (xA ^ yB))) | n) = xA & (X | n) = xA by A12, AFINSQ_1: 57;

            (( @ X) /^ (n + nA)) = yB & (( @ ( @ (xA ^ yB))) /^ n) = yB by A10, A13, AFINSQ_2: 12;

            then

             A15: ( eval (qB,X)) = 0 by A8, A9, A14, A6;

            reconsider Y = ( @ ( @ (yA ^ yB))) as N -element XFinSequence of NAT ;

            

             A16: ( eval ((qA *' qA),( @ (xA ^ Y)))) = (( eval (qA,( @ (xA ^ Y)))) * ( eval (qA,( @ (xA ^ Y))))) by POLYNOM2: 25

            .= ( 0 * 0 ) by A11, A12;

            

             A17: ( eval ((qB *' qB),( @ (xA ^ Y)))) = (( eval (qB,( @ (xA ^ Y)))) * ( eval (qB,( @ (xA ^ Y))))) by POLYNOM2: 25

            .= ( 0 * 0 ) by A15, A12;

            ( eval (Q,( @ (xA ^ Y)))) = (( eval ((qA *' qA),( @ (xA ^ Y)))) + ( eval ((qB *' qB),( @ (xA ^ Y))))) by POLYNOM2: 23

            .= 0 by A16, A17;

            hence thesis by A8;

          end;

          given xA be n -element XFinSequence of NAT , y1 be N -element XFinSequence of NAT such that

           A18: xA = y & ( eval (Q,( @ (xA ^ y1)))) = 0 ;

          reconsider yA = (y1 | nA), yB = (y1 /^ nA) as XFinSequence of NAT ;

          

           A19: nA <= (nA + nB) & ( len y1) = (nA + nB) by NAT_1: 11, CARD_1:def 7;

          then ( len yA) = nA by AFINSQ_1: 54;

          then

          reconsider yA as nA -element XFinSequence of NAT by CARD_1:def 7;

          ( len yB) = ((nA + nB) -' nA) by A19, AFINSQ_2:def 2

          .= nB by NAT_D: 34;

          then

          reconsider yB as nB -element XFinSequence of NAT by CARD_1:def 7;

          reconsider X = ( @ ((xA ^ yA) ^ yB)) as Function of (n + N), F_Real ;

          

           A21: ( len (xA ^ yA)) = (n + nA) by CARD_1:def 7;

          then (((xA ^ yA) ^ yB) | (n + nA)) = (xA ^ yA) by AFINSQ_1: 57;

          then

           A22: ( eval (pA,( @ (xA ^ yA)))) = ( eval (qA,X)) by A4;

          

           A23: X = (xA ^ (yA ^ yB)) by AFINSQ_1: 27;

          

           A24: ( len xA) = n by CARD_1:def 7;

          then

           A25: (( @ ( @ (xA ^ yB))) | n) = xA & (X | n) = xA by A23, AFINSQ_1: 57;

          (( @ X) /^ (n + nA)) = yB & (( @ ( @ (xA ^ yB))) /^ n) = yB by A21, A24, AFINSQ_2: 12;

          then

           A26: ( eval (pB,( @ (xA ^ yB)))) = ( eval (qB,X)) by A25, A6;

          reconsider eA = ( eval (qA,( @ (xA ^ y1)))) as Integer by INT_1:def 2;

          reconsider eB = ( eval (qB,( @ (xA ^ y1)))) as Integer by INT_1:def 2;

          reconsider eAA = (eA * eA), eBB = (eB * eB) as Element of NAT by INT_1: 3, XREAL_1: 63;

          

           A27: ( eval ((qA *' qA),( @ (xA ^ y1)))) = (( eval (qA,( @ (xA ^ y1)))) * ( eval (qA,( @ (xA ^ y1))))) by POLYNOM2: 25

          .= eAA;

          

           A28: ( eval ((qB *' qB),( @ (xA ^ y1)))) = (( eval (qB,( @ (xA ^ y1)))) * ( eval (qB,( @ (xA ^ y1))))) by POLYNOM2: 25

          .= eBB;

          ( eval (Q,( @ (xA ^ y1)))) = (( eval ((qA *' qA),( @ (xA ^ y1)))) + ( eval ((qB *' qB),( @ (xA ^ y1))))) by POLYNOM2: 23

          .= (eAA + eBB) by A27, A28;

          then eAA = 0 & eBB = 0 by A18;

          then

           A29: eA = 0 & eB = 0 by XCMPLX_1: 6;

          then

           A30: xA in A by A1, A22, A23;

          xA in B by A2, A29, A26, A23;

          hence thesis by A18, A30, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

      cluster (A \/ B) -> diophantine;

      coherence

      proof

        consider nA be Nat, pA be INT -valued Polynomial of (n + nA), F_Real such that

         A31: for s holds s in A iff ex x be n -element XFinSequence of NAT , y be nA -element XFinSequence of NAT st s = x & ( eval (pA,( @ (x ^ y)))) = 0 by Def6;

        consider nB be Nat, pB be INT -valued Polynomial of (n + nB), F_Real such that

         A32: for s holds s in B iff ex x be n -element XFinSequence of NAT , y be nB -element XFinSequence of NAT st s = x & ( eval (pB,( @ (x ^ y)))) = 0 by Def6;

        (A \/ B) is diophantine

        proof

          take N = (nA + nB);

          consider qA be Polynomial of ((n + nA) + nB), F_Real such that

           A33: ( rng qA) c= (( rng pA) \/ {( 0. F_Real )}) and

           A34: for x be Function of (n + nA), F_Real , y be Function of ((n + nA) + nB), F_Real st (y | (n + nA)) = x holds ( eval (pA,x)) = ( eval (qA,y)) by Th27;

          ( rng qA) c= INT by A33, INT_1:def 2;

          then

          reconsider qA as INT -valued Polynomial of (n + N), F_Real by RELAT_1:def 19;

          consider qB be Polynomial of ((n + nA) + nB), F_Real such that

           A35: ( rng qB) c= (( rng pB) \/ {( 0. F_Real )}) and

           A36: for XY be Function of (n + nB), F_Real , XanyY be Function of ((n + nA) + nB), F_Real st (XY | n) = (XanyY | n) & (( @ XY) /^ n) = (( @ XanyY) /^ (n + nA)) holds ( eval (pB,XY)) = ( eval (qB,XanyY)) by Th28;

          ( rng qB) c= INT by A35, INT_1:def 2;

          then

          reconsider qB as INT -valued Polynomial of (n + N), F_Real by RELAT_1:def 19;

          take Q = (qA *' qB);

          let y be object;

          thus y in (A \/ B) implies ex x be n -element XFinSequence of NAT , y1 be N -element XFinSequence of NAT st y = x & ( eval (Q,( @ (x ^ y1)))) = 0

          proof

            assume y in (A \/ B);

            per cases by XBOOLE_0:def 3;

              suppose y in A;

              then

              consider xA be n -element XFinSequence of NAT , yA be nA -element XFinSequence of NAT such that

               A38: y = xA & ( eval (pA,( @ (xA ^ yA)))) = 0 by A31;

              set yB = the nB -element XFinSequence of NAT ;

              reconsider X = ( @ ((xA ^ yA) ^ yB)) as Function of (n + N), F_Real ;

              ( len (xA ^ yA)) = (n + nA) by CARD_1:def 7;

              then (((xA ^ yA) ^ yB) | (n + nA)) = (xA ^ yA) by AFINSQ_1: 57;

              then

               A39: ( eval (qA,X)) = 0 by A38, A34;

              reconsider Y = ( @ ( @ (yA ^ yB))) as N -element XFinSequence of NAT ;

              ( eval (Q,( @ (xA ^ Y)))) = (( eval (qA,( @ (xA ^ Y)))) * ( eval (qB,( @ (xA ^ Y))))) by POLYNOM2: 25

              .= ( 0 * ( eval (qB,( @ (xA ^ Y))))) by A39, AFINSQ_1: 27;

              hence thesis by A38;

            end;

              suppose y in B;

              then

              consider xA be n -element XFinSequence of NAT , yB be nB -element XFinSequence of NAT such that

               A40: y = xA & ( eval (pB,( @ (xA ^ yB)))) = 0 by A32;

              set yA = the nA -element XFinSequence of NAT ;

              reconsider X = ( @ ((xA ^ yA) ^ yB)) as Function of (n + N), F_Real ;

              

               A41: ( len (xA ^ yA)) = (n + nA) by CARD_1:def 7;

              

               A42: X = (xA ^ (yA ^ yB)) by AFINSQ_1: 27;

              

               A43: ( len xA) = n by CARD_1:def 7;

              then

               A44: (( @ ( @ (xA ^ yB))) | n) = xA & (X | n) = xA by A42, AFINSQ_1: 57;

              

               A45: (( @ X) /^ (n + nA)) = yB & (( @ ( @ (xA ^ yB))) /^ n) = yB by A41, A43, AFINSQ_2: 12;

              reconsider Y = ( @ ( @ (yA ^ yB))) as N -element XFinSequence of NAT ;

              ( eval (Q,( @ (xA ^ Y)))) = (( eval (qA,( @ (xA ^ Y)))) * ( eval (qB,( @ (xA ^ Y))))) by POLYNOM2: 25

              .= (( eval (qA,( @ (xA ^ Y)))) * 0 ) by A45, A40, A44, A36, A42;

              hence thesis by A40;

            end;

          end;

          given xA be n -element XFinSequence of NAT , y1 be N -element XFinSequence of NAT such that

           A46: xA = y & ( eval (Q,( @ (xA ^ y1)))) = 0 ;

          reconsider yA = (y1 | nA), yB = (y1 /^ nA) as XFinSequence of NAT ;

          

           A47: nA <= (nA + nB) & ( len y1) = (nA + nB) by NAT_1: 11, CARD_1:def 7;

          then ( len yA) = nA by AFINSQ_1: 54;

          then

          reconsider yA as nA -element XFinSequence of NAT by CARD_1:def 7;

          ( len yB) = ((nA + nB) -' nA) by A47, AFINSQ_2:def 2

          .= nB by NAT_D: 34;

          then

          reconsider yB as nB -element XFinSequence of NAT by CARD_1:def 7;

          reconsider X = ( @ ((xA ^ yA) ^ yB)) as Function of (n + N), F_Real ;

          

           A49: ( len (xA ^ yA)) = (n + nA) by CARD_1:def 7;

          then (((xA ^ yA) ^ yB) | (n + nA)) = (xA ^ yA) by AFINSQ_1: 57;

          then

           A50: ( eval (pA,( @ (xA ^ yA)))) = ( eval (qA,X)) by A34;

          

           A51: X = (xA ^ (yA ^ yB)) by AFINSQ_1: 27;

          

           A52: ( len xA) = n by CARD_1:def 7;

          then

           A53: (( @ ( @ (xA ^ yB))) | n) = xA & (X | n) = xA by A51, AFINSQ_1: 57;

          (( @ X) /^ (n + nA)) = yB & (( @ ( @ (xA ^ yB))) /^ n) = yB by A49, A52, AFINSQ_2: 12;

          then

           A54: ( eval (pB,( @ (xA ^ yB)))) = ( eval (qB,X)) by A53, A36;

          reconsider eA = ( eval (qA,( @ (xA ^ y1)))) as Integer by INT_1:def 2;

          reconsider eB = ( eval (qB,( @ (xA ^ y1)))) as Integer by INT_1:def 2;

          ( eval (Q,( @ (xA ^ y1)))) = (( eval (qA,( @ (xA ^ y1)))) * ( eval (qB,( @ (xA ^ y1))))) by POLYNOM2: 25

          .= (eA * eB);

          then eA = 0 or eB = 0 by A46, XCMPLX_1: 6;

          then xA in A or xA in B by A31, A32, A54, A50, A51;

          hence thesis by A46, XBOOLE_0:def 3;

        end;

        hence thesis;

      end;

    end