hilbasis.miz



    begin

    theorem :: HILBASIS:1

    

     Th1: for A,B be FinSequence, f be Function st (( rng A) \/ ( rng B)) c= ( dom f) holds ex fA,fB be FinSequence st fA = (f * A) & fB = (f * B) & (f * (A ^ B)) = (fA ^ fB)

    proof

      let A,B be FinSequence, f be Function;

      assume

       A1: (( rng A) \/ ( rng B)) c= ( dom f);

      then

       A2: ( rng (A ^ B)) c= ( dom f) by FINSEQ_1: 31;

      then

      reconsider fAB = (f * (A ^ B)) as FinSequence by FINSEQ_1: 16;

      

       A3: ( rng B) c= (( rng A) \/ ( rng B)) by XBOOLE_1: 7;

      then

      reconsider fB = (f * B) as FinSequence by A1, FINSEQ_1: 16, XBOOLE_1: 1;

      

       A4: ( dom (f * B)) = ( dom B) by A1, A3, RELAT_1: 27, XBOOLE_1: 1;

      then

       A5: ( len fB) = ( len B) by FINSEQ_3: 29;

      

       A6: ( rng A) c= (( rng A) \/ ( rng B)) by XBOOLE_1: 7;

      then

      reconsider fA = (f * A) as FinSequence by A1, FINSEQ_1: 16, XBOOLE_1: 1;

      take fA, fB;

      

       A7: ( dom (f * (A ^ B))) = ( dom (A ^ B)) by A2, RELAT_1: 27;

      

       A8: ( dom (f * A)) = ( dom A) by A1, A6, RELAT_1: 27, XBOOLE_1: 1;

      then

       A9: ( len fA) = ( len A) by FINSEQ_3: 29;

       A10:

      now

        let k be Nat;

        assume 1 <= k & k <= ( len fAB);

        then

         A11: k in ( dom fAB) by FINSEQ_3: 25;

        per cases ;

          suppose

           A12: k in ( dom fA);

          

          hence ((fA ^ fB) . k) = (fA . k) by FINSEQ_1:def 7

          .= (f . (A . k)) by A12, FUNCT_1: 12

          .= (f . ((A ^ B) . k)) by A8, A12, FINSEQ_1:def 7

          .= (fAB . k) by A11, FUNCT_1: 12;

        end;

          suppose not k in ( dom fA);

          then

          consider n be Nat such that

           A13: n in ( dom B) and

           A14: k = (( len A) + n) by A8, A7, A11, FINSEQ_1: 25;

          

          thus (fAB . k) = (f . ((A ^ B) . k)) by A11, FUNCT_1: 12

          .= (f . (B . n)) by A13, A14, FINSEQ_1:def 7

          .= (fB . n) by A4, A13, FUNCT_1: 12

          .= ((fA ^ fB) . k) by A9, A4, A13, A14, FINSEQ_1:def 7;

        end;

      end;

      ( len fAB) = ( len (A ^ B)) by A7, FINSEQ_3: 29

      .= (( len fA) + ( len fB)) by A9, A5, FINSEQ_1: 22

      .= ( len (fA ^ fB)) by FINSEQ_1: 22;

      hence thesis by A10, FINSEQ_1: 14;

    end;

    theorem :: HILBASIS:2

    

     Th2: for b be bag of {} holds ( decomp b) = <* <* {} , {} *>*>

    proof

      let b be bag of {} ;

      

       A1: ( EmptyBag 0 ) = ( {} --> 0 );

      then ( divisors b) = <* {} *> by PRE_POLY: 67;

      then

       A2: ( len ( divisors b)) = 1 by FINSEQ_1: 39;

      

       A3: ( dom ( divisors b)) = ( dom ( decomp b)) by PRE_POLY:def 17;

      then 1 in ( dom ( decomp b)) by A2, FINSEQ_3: 25;

      

      then

       A4: (( decomp b) . 1) = (( decomp b) /. 1) by PARTFUN1:def 6

      .= <* {} , {} *> by A1, PRE_POLY: 71;

      ( len ( decomp b)) = 1 by A2, A3, FINSEQ_3: 29;

      hence thesis by A4, FINSEQ_1: 40;

    end;

    theorem :: HILBASIS:3

    

     Th3: for i,j be Nat, b be bag of j st i <= j holds (b | i) is Element of ( Bags i)

    proof

      let i,j be Nat, b be bag of j;

      assume

       A1: i <= j;

      ( Segm i) c= ( Segm j)

      proof

        let x be object;

        assume x in ( Segm i);

        then x in { y where y be Nat : y < i } by AXIOMS: 4;

        then

        consider x9 be Nat such that

         A2: x9 = x and

         A3: x9 < i;

        x9 < j by A1, A3, XXREAL_0: 2;

        then x9 in { y where y be Nat : y < j };

        hence thesis by A2, AXIOMS: 4;

      end;

      hence thesis by PRE_POLY:def 12;

    end;

    theorem :: HILBASIS:4

    

     Th4: for i,j be set, b1,b2 be bag of j, b19,b29 be bag of i st b19 = (b1 | i) & b29 = (b2 | i) & b1 divides b2 holds b19 divides b29

    proof

      let i,j be set, b1,b2 be bag of j, b19,b29 be bag of i;

      assume that

       A1: b19 = (b1 | i) & b29 = (b2 | i) and

       A2: b1 divides b2;

      now

        let k be object;

        

         A3: ( dom b19) = i by PARTFUN1:def 2

        .= ( dom b29) by PARTFUN1:def 2;

        per cases ;

          suppose

           A4: not k in ( dom b19);

          

          then (b19 . k) = {} by FUNCT_1:def 2

          .= (b29 . k) by A3, A4, FUNCT_1:def 2;

          hence (b19 . k) <= (b29 . k);

        end;

          suppose k in ( dom b19);

          then (b19 . k) = (b1 . k) & (b29 . k) = (b2 . k) by A1, A3, FUNCT_1: 47;

          hence (b19 . k) <= (b29 . k) by A2, PRE_POLY:def 11;

        end;

      end;

      hence thesis by PRE_POLY:def 11;

    end;

    theorem :: HILBASIS:5

    

     Th5: for i,j be set, b1,b2 be bag of j, b19,b29 be bag of i st b19 = (b1 | i) & b29 = (b2 | i) holds ((b1 -' b2) | i) = (b19 -' b29) & ((b1 + b2) | i) = (b19 + b29)

    proof

      let i,j be set, b1,b2 be bag of j, b19,b29 be bag of i;

      assume that

       A1: b19 = (b1 | i) and

       A2: b29 = (b2 | i);

      ( dom b1) = j by PARTFUN1:def 2;

      then

       A3: ( dom (b1 | i)) = (j /\ i) by RELAT_1: 61;

      ( dom b2) = j by PARTFUN1:def 2;

      then

       A4: ( dom (b2 | i)) = (j /\ i) by RELAT_1: 61;

      ( dom (b1 + b2)) = j by PARTFUN1:def 2;

      then

       A5: ( dom ((b1 + b2) | i)) = (j /\ i) by RELAT_1: 61;

       A6:

      now

        let x be object;

        assume

         A7: x in (j /\ i);

        

        hence (((b1 + b2) | i) . x) = ((b1 + b2) . x) by A5, FUNCT_1: 47

        .= ((b1 . x) + (b2 . x)) by PRE_POLY:def 5

        .= ((b19 . x) + (b2 . x)) by A1, A3, A7, FUNCT_1: 47

        .= ((b19 . x) + (b29 . x)) by A2, A4, A7, FUNCT_1: 47

        .= ((b19 + b29) . x) by PRE_POLY:def 5;

      end;

      ( dom (b1 -' b2)) = j by PARTFUN1:def 2;

      then

       A8: ( dom ((b1 -' b2) | i)) = (j /\ i) by RELAT_1: 61;

       A9:

      now

        let x be object;

        assume

         A10: x in (j /\ i);

        

        hence (((b1 -' b2) | i) . x) = ((b1 -' b2) . x) by A8, FUNCT_1: 47

        .= ((b1 . x) -' (b2 . x)) by PRE_POLY:def 6

        .= ((b19 . x) -' (b2 . x)) by A1, A3, A10, FUNCT_1: 47

        .= ((b19 . x) -' (b29 . x)) by A2, A4, A10, FUNCT_1: 47

        .= ((b19 -' b29) . x) by PRE_POLY:def 6;

      end;

      ( dom (b19 -' b29)) = i by PARTFUN1:def 2

      .= (j /\ i) by A1, A3, PARTFUN1:def 2;

      hence ((b1 -' b2) | i) = (b19 -' b29) by A8, A9, FUNCT_1: 2;

      ( dom (b19 + b29)) = i by PARTFUN1:def 2

      .= (j /\ i) by A1, A3, PARTFUN1:def 2;

      hence thesis by A5, A6, FUNCT_1: 2;

    end;

    definition

      let n,k be Nat, b be bag of n;

      :: HILBASIS:def1

      func b bag_extend k -> Element of ( Bags (n + 1)) means

      : Def1: (it | n) = b & (it . n) = k;

      existence

      proof

        set b1 = (b +* (n .--> k));

        

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

        

         A2: ( dom b1) = (( dom b) \/ ( dom (n .--> k))) by FUNCT_4:def 1

        .= (( dom b) \/ {n})

        .= (( Segm n) \/ {n}) by PARTFUN1:def 2

        .= ( Segm (n + 1)) by AFINSQ_1: 2;

        then b1 is ManySortedSet of (n + 1) by PARTFUN1:def 2, RELAT_1:def 18;

        then

        reconsider b1 as Element of ( Bags (n + 1)) by PRE_POLY:def 12;

        take b1;

        

         A3: ( dom (b1 | n)) = (( Segm (n + 1)) /\ ( Segm n)) by A2, RELAT_1: 61

        .= ((( Segm n) \/ {n}) /\ ( Segm n)) by AFINSQ_1: 2

        .= ( Segm n) by XBOOLE_1: 21;

        now

          let x be object;

          assume

           A4: x in n;

          then

           A5: x in (( dom b) \/ ( dom (n .--> k))) by A1, XBOOLE_0:def 3;

           A6:

          now

            assume x in ( dom (n .--> k));

            then x in {n};

            then

             A: x = n by TARSKI:def 1;

            then

            reconsider x as set;

             not x in x;

            hence contradiction by A4, A;

          end;

          

          thus ((b1 | n) . x) = (b1 . x) by A3, A4, FUNCT_1: 47

          .= (b . x) by A5, A6, FUNCT_4:def 1;

        end;

        hence (b1 | n) = b by A3, A1, FUNCT_1: 2;

        n in {n} by TARSKI:def 1;

        then

         A7: n in ( dom (n .--> k));

        then n in (( dom b) \/ ( dom (n .--> k))) by XBOOLE_0:def 3;

        

        hence (b1 . n) = ((n .--> k) . n) by A7, FUNCT_4:def 1

        .= k by FUNCOP_1: 72;

      end;

      uniqueness

      proof

        let b1,b2 be Element of ( Bags (n + 1));

        assume that

         A8: (b1 | n) = b and

         A9: (b1 . n) = k and

         A10: (b2 | n) = b and

         A11: (b2 . n) = k;

        

         A12: ( dom b1) = (n + 1) by PARTFUN1:def 2;

         A13:

        now

          let x be object;

          assume

           A14: x in ( Segm (n + 1));

          then

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

          per cases ;

            suppose x in {n};

            then x = n by TARSKI:def 1;

            hence (b1 . x) = (b2 . x) by A9, A11;

          end;

            suppose not x in {n};

            then x in n by A15, XBOOLE_0:def 3;

            then x in ((n + 1) /\ n) by A14, XBOOLE_0:def 4;

            then

             A16: x in ( dom b) by A8, A12, RELAT_1: 61;

            

            hence (b1 . x) = (b . x) by A8, FUNCT_1: 47

            .= (b2 . x) by A10, A16, FUNCT_1: 47;

          end;

        end;

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

        hence thesis by A12, A13, FUNCT_1: 2;

      end;

    end

    theorem :: HILBASIS:6

    

     Th6: for n be Nat holds ( EmptyBag (n + 1)) = (( EmptyBag n) bag_extend 0 )

    proof

      let n be Nat;

       A1:

      now

        let x be object;

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

        then

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

        per cases by A2, XBOOLE_0:def 3;

          suppose

           A3: x in n;

          

          thus (( EmptyBag (n + 1)) . x) = 0 by PBOOLE: 5

          .= (( EmptyBag n) . x) by PBOOLE: 5

          .= (((( EmptyBag n) bag_extend 0 ) | n) . x) by Def1

          .= ((( EmptyBag n) bag_extend 0 ) . x) by A3, FUNCT_1: 49;

        end;

          suppose

           A4: x in {n};

          

          thus (( EmptyBag (n + 1)) . x) = 0 by PBOOLE: 5

          .= ((( EmptyBag n) bag_extend 0 ) . n) by Def1

          .= ((( EmptyBag n) bag_extend 0 ) . x) by A4, TARSKI:def 1;

        end;

      end;

      ( dom ( EmptyBag (n + 1))) = (n + 1) & ( dom (( EmptyBag n) bag_extend 0 )) = (n + 1) by PARTFUN1:def 2;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: HILBASIS:7

    

     Th7: for n be Ordinal, b,b1 be bag of n holds b1 in ( rng ( divisors b)) iff b1 divides b

    proof

      let n be Ordinal, b,b1 be bag of n;

      consider S be non empty finite Subset of ( Bags n) such that

       A1: ( divisors b) = ( SgmX (( BagOrder n),S)) and

       A2: for p be bag of n holds p in S iff p divides b by PRE_POLY:def 16;

      ( field ( BagOrder n)) = ( Bags n) by ORDERS_1: 15;

      then

       A3: ( BagOrder n) linearly_orders S by ORDERS_1: 37, ORDERS_1: 38;

      hereby

        assume b1 in ( rng ( divisors b));

        then b1 in S by A1, A3, PRE_POLY:def 2;

        hence b1 divides b by A2;

      end;

      assume b1 divides b;

      then b1 in S by A2;

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

    end;

    definition

      let X be set, x be Element of X;

      :: HILBASIS:def2

      func UnitBag x -> Element of ( Bags X) equals (( EmptyBag X) +* (x,1));

      coherence by PRE_POLY:def 12;

    end

    theorem :: HILBASIS:8

    

     Th8: for X be non empty set, x be Element of X holds ( support ( UnitBag x)) = {x}

    proof

      let X be non empty set, x be Element of X;

      now

        let a be object;

        hereby

          assume

           A1: a in ( support ( UnitBag x));

          now

            assume a <> x;

            

            then ((( EmptyBag X) +* (x,1)) . a) = (( EmptyBag X) . a) by FUNCT_7: 32

            .= 0 by PBOOLE: 5;

            hence contradiction by A1, PRE_POLY:def 7;

          end;

          hence a in {x} by TARSKI:def 1;

        end;

        ( EmptyBag X) = (X --> 0 ) by PBOOLE:def 3;

        then

         A2: ( dom ( EmptyBag X)) = X;

        assume a in {x};

        then a = x by TARSKI:def 1;

        then (( UnitBag x) . a) = 1 by A2, FUNCT_7: 31;

        hence a in ( support ( UnitBag x)) by PRE_POLY:def 7;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: HILBASIS:9

    

     Th9: for X be non empty set, x be Element of X holds (( UnitBag x) . x) = 1 & for y be Element of X st x <> y holds (( UnitBag x) . y) = 0

    proof

      let X be non empty set, x be Element of X;

      

       A1: ( dom (X --> 0 )) = X;

      

      thus (( UnitBag x) . x) = (((X --> 0 ) +* (x,1)) . x) by PBOOLE:def 3

      .= 1 by A1, FUNCT_7: 31;

      let y be Element of X;

      assume x <> y;

      

      hence (( UnitBag x) . y) = (( EmptyBag X) . y) by FUNCT_7: 32

      .= 0 by PBOOLE: 5;

    end;

    theorem :: HILBASIS:10

    

     Th10: for X be non empty set, x1,x2 be Element of X st ( UnitBag x1) = ( UnitBag x2) holds x1 = x2

    proof

      let X be non empty set, x1,x2 be Element of X such that

       A1: ( UnitBag x1) = ( UnitBag x2) and

       A2: x1 <> x2;

      1 = (( UnitBag x2) . x1) by A1, Th9

      .= 0 by A2, Th9;

      hence contradiction;

    end;

    theorem :: HILBASIS:11

    

     Th11: for X be non empty Ordinal, x be Element of X, L be well-unital non trivial doubleLoopStr, e be Function of X, L holds ( eval (( UnitBag x),e)) = (e . x)

    proof

      let X be non empty Ordinal, x be Element of X, L be well-unital non trivial doubleLoopStr, e be Function of X, L;

      reconsider edx = (e . x) as Element of L;

      ( support ( UnitBag x)) = {x} by Th8;

      

      hence ( eval (( UnitBag x),e)) = (( power L) . ((e . x),(( UnitBag x) . x))) by POLYNOM2: 15

      .= (( power L) . ((e . x),( 0 + 1))) by Th9

      .= ((( power L) . (edx, 0 )) * edx) by GROUP_1:def 7

      .= (( 1_ L) * edx) by GROUP_1:def 7

      .= (e . x);

    end;

    definition

      let X be set, x be Element of X, L be unital non empty multLoopStr_0;

      :: HILBASIS:def3

      func 1_1 (x,L) -> Series of X, L equals (( 0_ (X,L)) +* (( UnitBag x),( 1_ L)));

      coherence ;

    end

    theorem :: HILBASIS:12

    

     Th12: for X be set, L be unital non trivial doubleLoopStr, x be Element of X holds (( 1_1 (x,L)) . ( UnitBag x)) = ( 1_ L) & for b be bag of X st b <> ( UnitBag x) holds (( 1_1 (x,L)) . b) = ( 0. L)

    proof

      let X be set, L be unital non trivial doubleLoopStr, x be Element of X;

      ( dom ( 0_ (X,L))) = ( dom (( Bags X) --> ( 0. L))) by POLYNOM1:def 8

      .= ( Bags X);

      hence (( 1_1 (x,L)) . ( UnitBag x)) = ( 1_ L) by FUNCT_7: 31;

      let b be bag of X;

      assume b <> ( UnitBag x);

      

      hence (( 1_1 (x,L)) . b) = (( 0_ (X,L)) . b) by FUNCT_7: 32

      .= ( 0. L) by POLYNOM1: 22;

    end;

    theorem :: HILBASIS:13

    

     Th13: for X be set, x be Element of X, L be add-associative right_zeroed right_complementable well-unital right-distributive non trivial doubleLoopStr holds ( Support ( 1_1 (x,L))) = {( UnitBag x)}

    proof

      let X be set, x be Element of X, L be add-associative right_zeroed right_complementable well-unital right-distributive non trivial doubleLoopStr;

      now

        let a be object;

        hereby

          assume

           A1: a in ( Support ( 1_1 (x,L)));

          then

          reconsider b = a as Element of ( Bags X);

          now

            assume a <> ( UnitBag x);

            

            then (( 1_1 (x,L)) . b) = (( 0_ (X,L)) . b) by FUNCT_7: 32

            .= ( 0. L) by POLYNOM1: 22;

            hence contradiction by A1, POLYNOM1:def 4;

          end;

          hence a in {( UnitBag x)} by TARSKI:def 1;

        end;

        assume

         A2: a in {( UnitBag x)};

        then a = ( UnitBag x) by TARSKI:def 1;

        then (( 1_1 (x,L)) . a) <> ( 0. L) by Th12;

        hence a in ( Support ( 1_1 (x,L))) by A2, POLYNOM1:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let X be Ordinal, x be Element of X, L be add-associative right_zeroed right_complementable well-unital right-distributive non trivial doubleLoopStr;

      cluster ( 1_1 (x,L)) -> finite-Support;

      coherence

      proof

        ( Support ( 1_1 (x,L))) = {( UnitBag x)} by Th13;

        hence thesis by POLYNOM1:def 5;

      end;

    end

    theorem :: HILBASIS:14

    

     Th14: for L be add-associative right_zeroed right_complementable well-unital right-distributive non trivial doubleLoopStr, X be non empty set, x1,x2 be Element of X st ( 1_1 (x1,L)) = ( 1_1 (x2,L)) holds x1 = x2

    proof

      let L be add-associative right_zeroed right_complementable well-unital right-distributive non trivial doubleLoopStr, X be non empty set, x1,x2 be Element of X such that

       A1: ( 1_1 (x1,L)) = ( 1_1 (x2,L)) and

       A2: x1 <> x2;

      ( 1_ L) = (( 1_1 (x2,L)) . ( UnitBag x1)) by A1, Th12

      .= ( 0. L) by A2, Th10, Th12;

      hence contradiction;

    end;

    theorem :: HILBASIS:15

    

     Th15: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, x be Element of ( Polynom-Ring L), p be sequence of L st x = p holds ( - x) = ( - p)

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, x be Element of ( Polynom-Ring L), p be sequence of L;

      assume

       A1: x = p;

      reconsider x9 = x as Polynomial of L by POLYNOM3:def 10;

       A2:

      now

        let i be object;

        assume

         A3: i in NAT ;

        then

        reconsider i9 = i as Element of NAT ;

        

        thus ((p - p) . i) = ((p . i9) - (p . i9)) by POLYNOM3: 27

        .= ( 0. L) by RLVECT_1: 15

        .= (( 0_. L) . i) by A3, FUNCOP_1: 7;

      end;

      reconsider mx = ( - x9) as Element of ( Polynom-Ring L) by POLYNOM3:def 10;

      

       A4: (p - p) = ( 0_. L) by A2;

      (x + mx) = (x9 + ( - x9)) by POLYNOM3:def 10

      .= ( 0. ( Polynom-Ring L)) by A1, A4, POLYNOM3:def 10;

      then x = ( - mx) by RLVECT_1: 6;

      hence thesis by A1, RLVECT_1: 17;

    end;

    theorem :: HILBASIS:16

    

     Th16: for L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, x,y be Element of ( Polynom-Ring L), p,q be sequence of L st x = p & y = q holds (x - y) = (p - q)

    proof

      let L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, x,y be Element of ( Polynom-Ring L), p,q be sequence of L;

      assume that

       A1: x = p and

       A2: y = q;

      

       A3: ( - y) = ( - q) by A2, Th15;

      

      thus (x - y) = (x + ( - y)) by RLVECT_1:def 11

      .= (p - q) by A1, A3, POLYNOM3:def 10;

    end;

    definition

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

      let I be non empty Subset of ( Polynom-Ring L);

      :: HILBASIS:def4

      func minlen (I) -> non empty Subset of I equals { x where x be Element of I : for x9,y9 be Polynomial of L st x9 = x & y9 in I holds ( len x9) <= ( len y9) };

      coherence

      proof

        I c= I;

        then

        reconsider I9 = I as non empty Subset of I;

        defpred P[ Element of I, Element of NAT ] means for p be Polynomial of L st $1 = p holds $2 = ( len p);

        set u = { x where x be Element of I : for x9,y9 be Polynomial of L st x9 = x & y9 in I holds ( len x9) <= ( len y9) };

         A1:

        now

          let x be Element of I;

          reconsider x9 = x as Polynomial of L by POLYNOM3:def 10;

          for p be Polynomial of L st x = p holds ( len x9) = ( len p);

          hence ex y be Element of NAT st P[x, y];

        end;

        consider f be Function of I, NAT such that

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

        ( min (f .: I9)) in (f .: I) by XXREAL_2:def 7;

        then

        consider x be object such that

         A3: x in ( dom f) and x in I and

         A4: ( min (f .: I9)) = (f . x) by FUNCT_1:def 6;

        reconsider x as Element of I by A3;

        now

          let x9,y9 be Polynomial of L;

          assume that

           A5: x9 = x and

           A6: y9 in I;

          ( dom f) = I by FUNCT_2:def 1;

          then (f . y9) in (f .: I) by A6, FUNCT_1:def 6;

          then (f . x) <= (f . y9) by A4, XXREAL_2:def 7;

          then ( len x9) <= (f . y9) by A2, A5;

          hence ( len x9) <= ( len y9) by A2, A6;

        end;

        then

         A7: x in u;

        u c= I

        proof

          let x be object;

          assume x in u;

          then ex x99 be Element of I st x99 = x & for x9,y9 be Polynomial of L st x9 = x99 & y9 in I holds ( len x9) <= ( len y9);

          hence thesis;

        end;

        hence thesis by A7;

      end;

    end

    theorem :: HILBASIS:17

    

     Th17: for L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, I be non empty Subset of ( Polynom-Ring L), i1,i2 be Polynomial of L st i1 in ( minlen I) & i2 in I holds i1 in I & ( len i1) <= ( len i2)

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, I be non empty Subset of ( Polynom-Ring L), i1,i2 be Polynomial of L;

      assume that

       A1: i1 in ( minlen I) and

       A2: i2 in I;

      ex i19 be Element of I st i19 = i1 & for x9,y9 be Polynomial of L st x9 = i19 & y9 in I holds ( len x9) <= ( len y9) by A1;

      hence thesis by A2;

    end;

    definition

      let L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, n be Nat, a be Element of L;

      :: HILBASIS:def5

      func monomial (a,n) -> Polynomial of L means

      : Def5: for x be Nat holds (x = n implies (it . x) = a) & (x <> n implies (it . x) = ( 0. L));

      existence

      proof

        reconsider x = (( 0_. L) +* (n,a)) as sequence of L;

        now

          let i be Nat;

          

           A1: i in NAT by ORDINAL1:def 12;

          assume i >= (n + 1);

          then i > n by NAT_1: 13;

          

          hence (x . i) = (( NAT --> ( 0. L)) . i) by FUNCT_7: 32

          .= ( 0. L) by A1, FUNCOP_1: 7;

        end;

        then

        reconsider x as Polynomial of L by ALGSEQ_1:def 1;

        now

          let i be Nat;

          

           A2: i in NAT by ORDINAL1:def 12;

          thus i = n implies (x . i) = a

          proof

            

             A3: ( dom ( 0_. L)) = NAT ;

            assume i = n;

            hence thesis by A2, A3, FUNCT_7: 31;

          end;

          thus i <> n implies (x . i) = ( 0. L)

          proof

            assume i <> n;

            

            hence (x . i) = (( NAT --> ( 0. L)) . i) by FUNCT_7: 32

            .= ( 0. L) by A2, FUNCOP_1: 7;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let u,v be Polynomial of L such that

         A4: for x be Nat holds (x = n implies (u . x) = a) & (x <> n implies (u . x) = ( 0. L)) and

         A5: for x be Nat holds (x = n implies (v . x) = a) & (x <> n implies (v . x) = ( 0. L));

        now

          let x be object;

          assume

           A6: x in NAT ;

          per cases ;

            suppose

             A7: x = n;

            

            hence (u . x) = a by A4

            .= (v . x) by A5, A7;

          end;

            suppose

             A8: x <> n;

            

            hence (u . x) = ( 0. L) by A4, A6

            .= (v . x) by A5, A6, A8;

          end;

        end;

        hence u = v;

      end;

    end

    theorem :: HILBASIS:18

    

     Th18: for L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, n be Element of NAT , a be Element of L holds (a <> ( 0. L) implies ( len ( monomial (a,n))) = (n + 1)) & (a = ( 0. L) implies ( len ( monomial (a,n))) = 0 ) & ( len ( monomial (a,n))) <= (n + 1)

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, n be Element of NAT , a be Element of L;

       A1:

      now

        assume

         A2: a = ( 0. L);

        now

          let i be Nat;

          assume i >= 0 ;

          per cases ;

            suppose i = n;

            thus (( monomial (a,n)) . i) = ( 0. L) by A2, Def5;

          end;

            suppose i <> n;

            hence (( monomial (a,n)) . i) = ( 0. L) by Def5;

          end;

        end;

        then 0 is_at_least_length_of ( monomial (a,n)) by ALGSEQ_1:def 2;

        hence ( len ( monomial (a,n))) = 0 by ALGSEQ_1:def 3;

      end;

      now

        now

          let i be Nat;

          assume i >= (n + 1);

          then i > n by NAT_1: 13;

          hence (( monomial (a,n)) . i) = ( 0. L) by Def5;

        end;

        then (n + 1) is_at_least_length_of ( monomial (a,n)) by ALGSEQ_1:def 2;

        then

         A3: ( len ( monomial (a,n))) <= (n + 1) by ALGSEQ_1:def 3;

        assume a <> ( 0. L);

        then (( monomial (a,n)) . n) <> ( 0. L) by Def5;

        then ( len ( monomial (a,n))) > n by ALGSEQ_1: 8;

        then ( len ( monomial (a,n))) >= (n + 1) by NAT_1: 13;

        hence ( len ( monomial (a,n))) = (n + 1) by A3, XXREAL_0: 1;

      end;

      hence thesis by A1;

    end;

    theorem :: HILBASIS:19

    

     Th19: for L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, n,x be Element of NAT , a be Element of L, p be Polynomial of L holds ((( monomial (a,n)) *' p) . (x + n)) = (a * (p . x))

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, n,x be Element of NAT , a be Element of L, p be Polynomial of L;

      consider r be FinSequence of the carrier of L such that

       A1: ( len r) = ((x + n) + 1) and

       A2: ((( monomial (a,n)) *' p) . (x + n)) = ( Sum r) and

       A3: for k be Element of NAT st k in ( dom r) holds (r . k) = ((( monomial (a,n)) . (k -' 1)) * (p . (((x + n) + 1) -' k))) by POLYNOM3:def 9;

      ( len r) = (n + (1 + x)) by A1;

      then

      consider b,c be FinSequence of the carrier of L such that

       A4: ( len b) = n and

       A5: ( len c) = (1 + x) and

       A6: r = (b ^ c) by FINSEQ_2: 23;

      consider d,e be FinSequence of the carrier of L such that

       A7: ( len d) = 1 and ( len e) = x and

       A8: c = (d ^ e) by A5, FINSEQ_2: 23;

      

       A9: ( dom d) c= ( dom c) by A8, FINSEQ_1: 26;

      now

        

         A10: ( dom b) c= ( dom r) by A6, FINSEQ_1: 26;

        let i be Element of NAT ;

        

         A11: (i - 1) < i by XREAL_1: 146;

        assume

         A12: i in ( dom b);

        then

         A13: i <= n by A4, FINSEQ_3: 25;

        1 <= i by A12, FINSEQ_3: 25;

        then

         A14: (i -' 1) = (i - 1) by XREAL_1: 233;

        

        thus (b . i) = (r . i) by A6, A12, FINSEQ_1:def 7

        .= ((( monomial (a,n)) . (i -' 1)) * (p . (((x + n) + 1) -' i))) by A3, A12, A10

        .= (( 0. L) * (p . (((x + n) + 1) -' i))) by A13, A14, A11, Def5

        .= ( 0. L);

      end;

      then

       A15: ( Sum b) = ( 0. L) by POLYNOM3: 1;

      now

        let i be Element of NAT ;

        

         A16: ((n + (1 + i)) -' 1) = (((n + i) + 1) -' 1)

        .= (n + i) by NAT_D: 34;

        assume

         A17: i in ( dom e);

        then

         A18: (1 + i) in ( dom c) by A7, A8, FINSEQ_1: 28;

        i >= 1 by A17, FINSEQ_3: 25;

        then (n + i) >= (n + 1) by XREAL_1: 6;

        then

         A19: (n + i) > n by NAT_1: 13;

        

        thus (e . i) = (c . (1 + i)) by A7, A8, A17, FINSEQ_1:def 7

        .= (r . (n + (1 + i))) by A4, A6, A18, FINSEQ_1:def 7

        .= ((( monomial (a,n)) . ((n + (1 + i)) -' 1)) * (p . (((x + n) + 1) -' (n + (1 + i))))) by A3, A4, A6, A18, FINSEQ_1: 28

        .= (( 0. L) * (p . (((x + n) + 1) -' (n + (1 + i))))) by A19, A16, Def5

        .= ( 0. L);

      end;

      then

       A20: ( Sum e) = ( 0. L) by POLYNOM3: 1;

      

       A21: 1 in ( dom d) by A7, FINSEQ_3: 25;

      

      then (d . 1) = (c . 1) by A8, FINSEQ_1:def 7

      .= (r . (n + 1)) by A4, A6, A21, A9, FINSEQ_1:def 7

      .= ((( monomial (a,n)) . ((n + 1) -' 1)) * (p . (((x + n) + 1) -' (n + 1)))) by A3, A4, A6, A21, A9, FINSEQ_1: 28

      .= ((( monomial (a,n)) . n) * (p . ((x + (n + 1)) -' (n + 1)))) by NAT_D: 34

      .= ((( monomial (a,n)) . n) * (p . x)) by NAT_D: 34

      .= (a * (p . x)) by Def5;

      then d = <*(a * (p . x))*> by A7, FINSEQ_1: 40;

      then ( Sum d) = (a * (p . x)) by RLVECT_1: 44;

      

      then ( Sum c) = ((a * (p . x)) + ( 0. L)) by A8, A20, RLVECT_1: 41

      .= (a * (p . x)) by RLVECT_1: 4;

      

      hence ((( monomial (a,n)) *' p) . (x + n)) = (( 0. L) + (a * (p . x))) by A2, A6, A15, RLVECT_1: 41

      .= (a * (p . x)) by RLVECT_1: 4;

    end;

    theorem :: HILBASIS:20

    

     Th20: for L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, n,x be Element of NAT , a be Element of L, p be Polynomial of L holds ((p *' ( monomial (a,n))) . (x + n)) = ((p . x) * a)

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, n,x be Element of NAT , a be Element of L, p be Polynomial of L;

      consider r be FinSequence of the carrier of L such that

       A1: ( len r) = ((x + n) + 1) and

       A2: ((p *' ( monomial (a,n))) . (x + n)) = ( Sum r) and

       A3: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (( monomial (a,n)) . (((x + n) + 1) -' k))) by POLYNOM3:def 9;

      ( len r) = (x + (n + 1)) by A1;

      then

      consider b,c be FinSequence of the carrier of L such that

       A4: ( len b) = x and

       A5: ( len c) = (n + 1) and

       A6: r = (b ^ c) by FINSEQ_2: 23;

      consider d,e be FinSequence of the carrier of L such that

       A7: ( len d) = 1 and

       A8: ( len e) = n and

       A9: c = (d ^ e) by A5, FINSEQ_2: 23;

      

       A10: ( dom d) c= ( dom c) by A9, FINSEQ_1: 26;

      now

        let i be Element of NAT ;

        

         A11: n > (n - 1) by XREAL_1: 146;

        assume

         A12: i in ( dom e);

        then

         A13: (1 + i) in ( dom c) by A7, A9, FINSEQ_1: 28;

        i <= n by A8, A12, FINSEQ_3: 25;

        then (x + i) <= (x + n) by XREAL_1: 6;

        then ((x + i) + 1) <= ((x + n) + 1) by XREAL_1: 6;

        then

         A14: (((x + n) + 1) -' (x + (1 + i))) = (((x + n) + 1) - (x + (1 + i))) by XREAL_1: 233;

        1 <= i by A12, FINSEQ_3: 25;

        then

         A15: (n - i) <= (n - 1) by XREAL_1: 13;

        

        thus (e . i) = (c . (1 + i)) by A7, A9, A12, FINSEQ_1:def 7

        .= (r . (x + (1 + i))) by A4, A6, A13, FINSEQ_1:def 7

        .= ((p . ((x + (1 + i)) -' 1)) * (( monomial (a,n)) . (((x + n) + 1) -' (x + (1 + i))))) by A3, A4, A6, A13, FINSEQ_1: 28

        .= ((p . ((x + (1 + i)) -' 1)) * ( 0. L)) by A14, A15, A11, Def5

        .= ( 0. L);

      end;

      then

       A16: ( Sum e) = ( 0. L) by POLYNOM3: 1;

      now

        let i be Element of NAT ;

        

         A17: ( dom b) c= ( dom r) by A6, FINSEQ_1: 26;

        assume

         A18: i in ( dom b);

        then i <= x by A4, FINSEQ_3: 25;

        then (i + n) <= (x + n) by XREAL_1: 6;

        then (i + n) < ((x + n) + 1) by NAT_1: 13;

        then

         A19: n < (((x + n) + 1) - i) by XREAL_1: 20;

        then

         A20: (((x + n) + 1) - i) = (((x + n) + 1) -' i) by XREAL_0:def 2;

        

        thus (b . i) = (r . i) by A6, A18, FINSEQ_1:def 7

        .= ((p . (i -' 1)) * (( monomial (a,n)) . (((x + n) + 1) -' i))) by A3, A18, A17

        .= ((p . (i -' 1)) * ( 0. L)) by A19, A20, Def5

        .= ( 0. L);

      end;

      then

       A21: ( Sum b) = ( 0. L) by POLYNOM3: 1;

      

       A22: 1 in ( dom d) by A7, FINSEQ_3: 25;

      

      then (d . 1) = (c . 1) by A9, FINSEQ_1:def 7

      .= (r . (x + 1)) by A4, A6, A22, A10, FINSEQ_1:def 7

      .= ((p . ((x + 1) -' 1)) * (( monomial (a,n)) . (((x + n) + 1) -' (x + 1)))) by A3, A4, A6, A22, A10, FINSEQ_1: 28

      .= ((p . x) * (( monomial (a,n)) . ((n + (x + 1)) -' (x + 1)))) by NAT_D: 34

      .= ((p . x) * (( monomial (a,n)) . n)) by NAT_D: 34

      .= ((p . x) * a) by Def5;

      then d = <*((p . x) * a)*> by A7, FINSEQ_1: 40;

      then ( Sum d) = ((p . x) * a) by RLVECT_1: 44;

      

      then ( Sum c) = (((p . x) * a) + ( 0. L)) by A9, A16, RLVECT_1: 41

      .= ((p . x) * a) by RLVECT_1: 4;

      

      hence ((p *' ( monomial (a,n))) . (x + n)) = (( 0. L) + ((p . x) * a)) by A2, A6, A21, RLVECT_1: 41

      .= ((p . x) * a) by RLVECT_1: 4;

    end;

    theorem :: HILBASIS:21

    

     Th21: for L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, p,q be Polynomial of L holds ( len (p *' q)) <= ((( len p) + ( len q)) -' 1)

    proof

      let L be right_zeroed add-associative right_complementable well-unital distributive non empty doubleLoopStr, p,q be Polynomial of L;

      now

        let i be Nat;

        

         A1: ((( len p) + ( len q)) -' 1) >= ((( len p) + ( len q)) - 1) by XREAL_0:def 2;

        i in NAT by ORDINAL1:def 12;

        then

        consider r be FinSequence of the carrier of L such that

         A2: ( len r) = (i + 1) and

         A3: ((p *' q) . i) = ( Sum r) and

         A4: for k be Element of NAT st k in ( dom r) holds (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by POLYNOM3:def 9;

        assume i >= ((( len p) + ( len q)) -' 1);

        then i >= (( len p) + (( len q) - 1)) by A1, XXREAL_0: 2;

        then ( len p) <= (i - (( len q) - 1)) by XREAL_1: 19;

        then

         A5: ( - ( len p)) >= ( - ((i - ( len q)) + 1)) by XREAL_1: 24;

        now

          let k be Element of NAT ;

          assume

           A6: k in ( dom r);

          then

           A7: (r . k) = ((p . (k -' 1)) * (q . ((i + 1) -' k))) by A4;

          k in ( Seg ( len r)) by A6, FINSEQ_1:def 3;

          then k <= (i + 1) by A2, FINSEQ_1: 1;

          then

           A8: ((i + 1) - k) >= 0 by XREAL_1: 48;

          per cases ;

            suppose (k -' 1) < ( len p);

            then (k - 1) < ( len p) by XREAL_0:def 2;

            then ( - (k - 1)) > ( - ( len p)) by XREAL_1: 24;

            then (1 - k) > ((( len q) - 1) - i) by A5, XXREAL_0: 2;

            then (i + (1 - k)) > (( len q) - 1) by XREAL_1: 19;

            then ((i + 1) -' k) > (( len q) - 1) by A8, XREAL_0:def 2;

            then ((i + 1) -' k) >= ((( len q) - 1) + 1) by INT_1: 7;

            then (q . ((i + 1) -' k)) = ( 0. L) by ALGSEQ_1: 8;

            hence (r . k) = ( 0. L) by A7;

          end;

            suppose (k -' 1) >= ( len p);

            then (p . (k -' 1)) = ( 0. L) by ALGSEQ_1: 8;

            hence (r . k) = ( 0. L) by A7;

          end;

        end;

        hence ((p *' q) . i) = ( 0. L) by A3, POLYNOM3: 1;

      end;

      then ((( len p) + ( len q)) -' 1) is_at_least_length_of (p *' q) by ALGSEQ_1:def 2;

      hence thesis by ALGSEQ_1:def 3;

    end;

    begin

    theorem :: HILBASIS:22

    

     Th22: for R,S be non empty doubleLoopStr, I be Ideal of R, P be Function of R, S st P is RingIsomorphism holds (P .: I) is Ideal of S

    proof

      let R,S be non empty doubleLoopStr, I be Ideal of R, P be Function of R, S;

      set Q = (P .: I);

      assume

       A1: P is RingIsomorphism;

       A2:

      now

        let p,x be Element of S;

        assume x in Q;

        then

        consider x9 be object such that

         A3: x9 in the carrier of R and

         A4: x9 in I and

         A5: x = (P . x9) by FUNCT_2: 64;

        reconsider x9 as Element of R by A3;

        

         A6: P is RingMonomorphism RingEpimorphism by A1;

        then P is onto;

        then

        consider p9 be object such that

         A7: p9 in ( dom P) and

         A8: p = (P . p9) by FUNCT_1:def 3;

        reconsider p9 as Element of R by A7;

        

         A9: (p9 * x9) in I by A4, IDEAL_1:def 2;

        P is RingHomomorphism by A6;

        then P is multiplicative;

        then (p * x) = (P . (p9 * x9)) by A5, A8;

        hence (p * x) in Q by A9, FUNCT_2: 35;

      end;

       A10:

      now

        let p,x be Element of S;

        assume x in Q;

        then

        consider x9 be object such that

         A11: x9 in the carrier of R and

         A12: x9 in I and

         A13: x = (P . x9) by FUNCT_2: 64;

        reconsider x9 as Element of R by A11;

        

         A14: P is RingMonomorphism RingEpimorphism by A1;

        then P is onto;

        then

        consider p9 be object such that

         A15: p9 in ( dom P) and

         A16: p = (P . p9) by FUNCT_1:def 3;

        reconsider p9 as Element of R by A15;

        

         A17: (x9 * p9) in I by A12, IDEAL_1:def 3;

        P is RingHomomorphism by A14;

        then P is multiplicative;

        then (x * p) = (P . (x9 * p9)) by A13, A16;

        hence (x * p) in Q by A17, FUNCT_2: 35;

      end;

      now

        let x,y be Element of S;

        assume that

         A18: x in Q and

         A19: y in Q;

        consider x9 be object such that

         A20: x9 in the carrier of R and

         A21: x9 in I and

         A22: x = (P . x9) by A18, FUNCT_2: 64;

        consider y9 be object such that

         A23: y9 in the carrier of R and

         A24: y9 in I and

         A25: y = (P . y9) by A19, FUNCT_2: 64;

        reconsider x9, y9 as Element of R by A20, A23;

        

         A26: (x9 + y9) in I by A21, A24, IDEAL_1:def 1;

        P is RingMonomorphism RingEpimorphism by A1;

        then P is additive;

        then (x + y) = (P . (x9 + y9)) by A22, A25;

        hence (x + y) in Q by A26, FUNCT_2: 35;

      end;

      hence thesis by A2, A10, IDEAL_1:def 1, IDEAL_1:def 2, IDEAL_1:def 3;

    end;

    theorem :: HILBASIS:23

    

     Th23: for R,S be add-associative right_zeroed right_complementable non empty doubleLoopStr, f be Function of R, S st f is RingHomomorphism holds (f . ( 0. R)) = ( 0. S)

    proof

      let R,S be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let f be Function of R, S;

      assume f is RingHomomorphism;

      then

       A1: f is additive;

      (f . ( 0. R)) = (f . (( 0. R) + ( 0. R))) by RLVECT_1: 4

      .= ((f . ( 0. R)) + (f . ( 0. R))) by A1;

      

      then ( 0. S) = (((f . ( 0. R)) + (f . ( 0. R))) + ( - (f . ( 0. R)))) by RLVECT_1:def 10

      .= ((f . ( 0. R)) + ((f . ( 0. R)) + ( - (f . ( 0. R))))) by RLVECT_1:def 3

      .= ((f . ( 0. R)) + ( 0. S)) by RLVECT_1:def 10

      .= (f . ( 0. R)) by RLVECT_1: 4;

      hence thesis;

    end;

    theorem :: HILBASIS:24

    

     Th24: for R,S be add-associative right_zeroed right_complementable non empty doubleLoopStr, F be non empty Subset of R, G be non empty Subset of S, P be Function of R, S, lc be LinearCombination of F, LC be LinearCombination of G, E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:] st P is RingHomomorphism & ( len lc) = ( len LC) & E represents lc & (for i be set st i in ( dom LC) holds (LC . i) = (((P . ((E /. i) `1_3 )) * (P . ((E /. i) `2_3 ))) * (P . ((E /. i) `3_3 )))) holds (P . ( Sum lc)) = ( Sum LC)

    proof

      let R,S be add-associative right_zeroed right_complementable non empty doubleLoopStr, F be non empty Subset of R, G be non empty Subset of S, P be Function of R, S, lc be LinearCombination of F, LC be LinearCombination of G, E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:] such that

       A1: P is RingHomomorphism and

       A2: ( len lc) = ( len LC) and

       A3: E represents lc and

       A4: for i be set st i in ( dom LC) holds (LC . i) = (((P . ((E /. i) `1_3 )) * (P . ((E /. i) `2_3 ))) * (P . ((E /. i) `3_3 )));

      defpred P[ Nat] means for lc9 be LinearCombination of F, LC9 be LinearCombination of G st lc9 = (lc | ( Seg $1)) & LC9 = (LC | ( Seg $1)) holds (P . ( Sum lc9)) = ( Sum LC9);

      

       A5: P is additive multiplicative by A1;

      

       A6: ( dom lc) = ( dom LC) by A2, FINSEQ_3: 29;

      

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

      proof

        let k be Nat;

        assume

         A8: P[k];

        thus P[(k + 1)]

        proof

          let lc9 be LinearCombination of F, LC9 be LinearCombination of G;

          assume that

           A9: lc9 = (lc | ( Seg (k + 1))) and

           A10: LC9 = (LC | ( Seg (k + 1)));

          per cases ;

            suppose

             A11: ( len lc) < (k + 1);

            then

             A12: ( len lc) <= k by NAT_1: 13;

            

             A13: lc9 = lc by A9, A11, FINSEQ_3: 49

            .= (lc | ( Seg k)) by A12, FINSEQ_3: 49;

            LC9 = LC by A2, A10, A11, FINSEQ_3: 49

            .= (LC | ( Seg k)) by A2, A12, FINSEQ_3: 49;

            hence thesis by A8, A13;

          end;

            suppose

             A14: ( len lc) >= (k + 1);

            set i = (k + 1);

            reconsider LCk = (LC | ( Seg k)) as LinearCombination of G by IDEAL_1: 41;

            reconsider lck = (lc | ( Seg k)) as LinearCombination of F by IDEAL_1: 41;

            1 <= (k + 1) by NAT_1: 11;

            then

             A15: (k + 1) in ( dom lc) by A14, FINSEQ_3: 25;

            then

             A16: (lc . (k + 1)) = (lc /. (k + 1)) by PARTFUN1:def 6;

            

             A17: (LC . (k + 1)) = (LC /. (k + 1)) by A6, A15, PARTFUN1:def 6;

            (lc | ( Seg (k + 1))) = (lck ^ <*(lc . (k + 1))*>) by A15, FINSEQ_5: 10;

            

            hence (P . ( Sum lc9)) = (P . (( Sum lck) + (lc /. (k + 1)))) by A9, A16, FVSUM_1: 71

            .= ((P . ( Sum lck)) + (P . (lc /. (k + 1)))) by A5

            .= (( Sum LCk) + (P . (lc /. (k + 1)))) by A8

            .= (( Sum LCk) + (P . ((((E /. i) `1_3 ) * ((E /. i) `2_3 )) * ((E /. i) `3_3 )))) by A3, A15, A16

            .= (( Sum LCk) + ((P . (((E /. i) `1_3 ) * ((E /. i) `2_3 ))) * (P . ((E /. i) `3_3 )))) by A5

            .= (( Sum LCk) + (((P . ((E /. i) `1_3 )) * (P . ((E /. i) `2_3 ))) * (P . ((E /. i) `3_3 )))) by A5

            .= (( Sum LCk) + (LC /. (k + 1))) by A4, A6, A15, A17

            .= ( Sum (LCk ^ <*(LC /. (k + 1))*>)) by FVSUM_1: 71

            .= ( Sum LC9) by A6, A10, A15, A17, FINSEQ_5: 10;

          end;

        end;

      end;

      

       A18: lc = (lc | ( Seg ( len lc))) & LC = (LC | ( Seg ( len LC))) by FINSEQ_3: 49;

      

       A19: P[ 0 ]

      proof

        let lc9 be LinearCombination of F, LC9 be LinearCombination of G such that

         A20: lc9 = (lc | ( Seg 0 ) qua set) and

         A21: LC9 = (LC | ( Seg 0 ) qua set);

        

        thus (P . ( Sum lc9)) = (P . ( Sum ( <*> the carrier of R))) by A20

        .= (P . ( 0. R)) by RLVECT_1: 43

        .= ( 0. S) by A1, Th23

        .= ( Sum ( <*> the carrier of S)) by RLVECT_1: 43

        .= ( Sum LC9) by A21;

      end;

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

      hence thesis by A2, A18;

    end;

    theorem :: HILBASIS:25

    

     Th25: for R,S be non empty doubleLoopStr, P be Function of R, S st P is RingIsomorphism holds (P " ) is RingIsomorphism

    proof

      let R,S be non empty doubleLoopStr, P be Function of R, S;

      assume

       A1: P is RingIsomorphism;

      then

       A2: P is RingEpimorphism;

      then

       A3: P is onto;

      

       A4: P is one-to-one by A1;

      

       A5: P is additive multiplicative unity-preserving by A2;

      for x,y be Element of S holds ((P " ) . (x + y)) = (((P " ) . x) + ((P " ) . y)) & ((P " ) . (x * y)) = (((P " ) . x) * ((P " ) . y)) & ((P " ) . ( 1_ S)) = ( 1_ R)

      proof

        

         A6: P is onto by A3;

        

         A7: ((P " ) . ( 1_ S)) = ((P " ) . (P . ( 1_ R))) by A5, GROUP_1:def 13

        .= ((P qua Function " ) . (P . ( 1_ R))) by A4, A6, TOPS_2:def 4

        .= ( 1_ R) by A4, FUNCT_2: 26;

        let x,y be Element of S;

        consider x9 be object such that

         A8: x9 in the carrier of R and

         A9: (P . x9) = x by A3, FUNCT_2: 11;

        reconsider x9 as Element of R by A8;

        

         A10: x9 = ((P qua Function " ) . (P . x9)) by A4, FUNCT_2: 26

        .= ((P " ) . x) by A4, A9, A6, TOPS_2:def 4;

        consider y9 be object such that

         A11: y9 in the carrier of R and

         A12: (P . y9) = y by A3, FUNCT_2: 11;

        reconsider y9 as Element of R by A11;

        

         A13: y9 = ((P qua Function " ) . (P . y9)) by A4, FUNCT_2: 26

        .= ((P " ) . y) by A6, A4, A12, TOPS_2:def 4;

        

         A14: ((P " ) . (x * y)) = ((P " ) . (P . (x9 * y9))) by A5, A9, A12

        .= ((P qua Function " ) . (P . (x9 * y9))) by A4, A6, TOPS_2:def 4

        .= (((P " ) . x) * ((P " ) . y)) by A4, A10, A13, FUNCT_2: 26;

        ((P " ) . (x + y)) = ((P " ) . (P . (x9 + y9))) by A5, A9, A12

        .= ((P qua Function " ) . (P . (x9 + y9))) by A4, A6, TOPS_2:def 4

        .= (((P " ) . x) + ((P " ) . y)) by A4, A10, A13, FUNCT_2: 26;

        hence thesis by A14, A7;

      end;

      then (P " ) is additive multiplicative unity-preserving by GROUP_1:def 13;

      then

       A15: (P " ) is RingHomomorphism;

      

       A16: ( rng P) = ( [#] S) by A3;

      then ( rng (P " )) = ( [#] R) by A4, TOPS_2: 49;

      then (P " ) is onto;

      then

       A17: (P " ) is RingEpimorphism by A15;

      (P " ) is one-to-one by A4, A16, TOPS_2: 50;

      hence thesis by A17;

    end;

    theorem :: HILBASIS:26

    

     Th26: for R,S be Abelian add-associative right_zeroed right_complementable associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of R, P be Function of R, S st P is RingIsomorphism holds (P .: (F -Ideal )) = ((P .: F) -Ideal )

    proof

      let R,S be Abelian add-associative right_zeroed right_complementable associative distributive well-unital non empty doubleLoopStr, F be non empty Subset of R, P be Function of R, S;

      assume

       A1: P is RingIsomorphism;

      now

        let x be object;

        

         A2: ( dom P) = the carrier of R by FUNCT_2:def 1;

        assume

         A3: x in ((P .: F) -Ideal );

        then

        consider lc be LinearCombination of (P .: F) such that

         A4: x = ( Sum lc) by IDEAL_1: 60;

        consider E be FinSequence of [:the carrier of S, the carrier of S, the carrier of S:] such that

         A5: E represents lc by IDEAL_1: 35;

        P is RingMonomorphism by A1;

        then

         A6: P is one-to-one;

        

         A7: P is onto by A1;

        then

         A8: (P qua Function " ) = (P " ) by A6, TOPS_2:def 4;

        ((P qua Function " ) .: (P .: F)) = (P qua Function " (P .: F)) by A6, FUNCT_1: 85;

        then

        consider lc9 be LinearCombination of F such that

         A9: ( len lc) = ( len lc9) & for i be set st i in ( dom lc9) holds (lc9 . i) = ((((P " ) . ((E /. i) `1_3 )) * ((P " ) . ((E /. i) `2_3 ))) * ((P " ) . ((E /. i) `3_3 ))) by A6, A8, A5, FUNCT_1: 82, IDEAL_1: 36;

        (P " ) is RingIsomorphism by A1, Th25;

        then (P " ) is RingMonomorphism;

        then (P " ) is RingHomomorphism;

        then ((P " ) . x) = ( Sum lc9) by A4, A5, A9, Th24;

        then ((P " ) . x) in (F -Ideal ) by IDEAL_1: 60;

        then (P . ((P " ) . x)) in (P .: (F -Ideal )) by A2, FUNCT_1:def 6;

        hence x in (P .: (F -Ideal )) by A3, A6, A7, A8, FUNCT_1: 35;

      end;

      then

       A10: ((P .: F) -Ideal ) c= (P .: (F -Ideal ));

      now

        let x be object;

        assume x in (P .: (F -Ideal ));

        then

        consider x9 be object such that x9 in the carrier of R and

         A11: x9 in (F -Ideal ) and

         A12: x = (P . x9) by FUNCT_2: 64;

        consider lc9 be LinearCombination of F such that

         A13: x9 = ( Sum lc9) by A11, IDEAL_1: 60;

        consider E be FinSequence of [:the carrier of R, the carrier of R, the carrier of R:] such that

         A14: E represents lc9 by IDEAL_1: 35;

        consider lc be LinearCombination of (P .: F) such that

         A15: ( len lc9) = ( len lc) & for i be set st i in ( dom lc) holds (lc . i) = (((P . ((E /. i) `1_3 )) * (P . ((E /. i) `2_3 ))) * (P . ((E /. i) `3_3 ))) by A14, IDEAL_1: 36;

        P is RingMonomorphism by A1;

        then P is RingHomomorphism;

        then x = ( Sum lc) by A12, A13, A14, A15, Th24;

        hence x in ((P .: F) -Ideal ) by IDEAL_1: 60;

      end;

      then (P .: (F -Ideal )) c= ((P .: F) -Ideal );

      hence thesis by A10, XBOOLE_0:def 10;

    end;

    theorem :: HILBASIS:27

    

     Th27: for R,S be Abelian add-associative right_zeroed right_complementable associative distributive well-unital non empty doubleLoopStr, P be Function of R, S st P is RingIsomorphism & R is Noetherian holds S is Noetherian

    proof

      let R,S be Abelian add-associative right_zeroed right_complementable associative distributive well-unital non empty doubleLoopStr, P be Function of R, S;

      assume that

       A1: P is RingIsomorphism and

       A2: R is Noetherian;

      now

        P is RingEpimorphism by A1;

        then

         A3: P is onto;

        let I be Ideal of S;

        P is RingMonomorphism by A1;

        then

         A4: P is one-to-one;

        reconsider PI = ((P " ) .: I) as Ideal of R by A1, Th22, Th25;

        PI is finitely_generated by A2;

        then

        consider F be non empty finite Subset of R such that

         A5: ((P " ) .: I) = (F -Ideal );

        P is onto by A3;

        then (P " ) = (P qua Function " ) by A4, TOPS_2:def 4;

        then (P .: ((P " ) .: I)) = (P .: (P " I)) by A4, FUNCT_1: 85;

        then (P .: ((P " ) .: I)) = I by A3, FUNCT_1: 77;

        then I = ((P .: F) -Ideal ) by A1, A5, Th26;

        hence I is finitely_generated;

      end;

      hence thesis;

    end;

    theorem :: HILBASIS:28

    

     Th28: for R be add-associative right_zeroed right_complementable associative Abelian distributive well-unital non trivial doubleLoopStr holds ex P be Function of R, ( Polynom-Ring ( 0 ,R)) st P is RingIsomorphism

    proof

      deffunc F( object) = (( Bags {} ) --> $1);

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

      consider P be Function such that

       A1: ( dom P) = the carrier of R and

       A2: for x be object st x in the carrier of R holds (P . x) = F(x) from FUNCT_1:sch 3;

      now

        let y be object;

        hereby

          assume y in ( rng P);

          then

          consider x be object such that

           A3: x in the carrier of R and

           A4: y = (P . x) by A1, FUNCT_1:def 3;

          reconsider x as Element of R by A3;

          reconsider y9 = (( Bags {} ) --> x) as Function of ( Bags {} ), R;

          ( Support y9) is finite by PRE_POLY: 51;

          then y9 is finite-Support Series of 0 , R by POLYNOM1:def 5;

          then y9 in the carrier of ( Polynom-Ring ( 0 ,R)) by POLYNOM1:def 11;

          hence y in the carrier of ( Polynom-Ring ( 0 ,R)) by A2, A4;

        end;

        assume y in the carrier of ( Polynom-Ring ( 0 ,R));

        then

        reconsider y9 = y as Function of ( Bags {} ), R by POLYNOM1:def 11;

        ( dom y9) = ( Bags {} ) by FUNCT_2:def 1;

        then ( rng y9) = {(y9 . {} )} by FUNCT_1: 4, PRE_POLY: 51;

        then (y9 . {} ) in ( rng y9) by TARSKI:def 1;

        then

        reconsider x = (y9 . {} ) as Element of R;

        y9 = (( Bags {} ) --> (y9 . {} ));

        then y = (P . x) by A2;

        hence y in ( rng P) by A1, FUNCT_1:def 3;

      end;

      then

       A7: ( rng P) = the carrier of ( Polynom-Ring ( 0 ,R)) by TARSKI: 2;

      then

      reconsider P as Function of R, ( Polynom-Ring ( 0 ,R)) by A1, FUNCT_2: 1;

      

       A8: P is onto by A7;

      

       A9: ( EmptyBag {} ) = ( {} --> 0 );

      now

        let x,y be Element of R;

        reconsider Px = (P . x), Py = (P . y), Pxy = (P . (x + y)) as Polynomial of 0 , R by POLYNOM1:def 11;

        now

          let z be bag of 0 ;

          

           A10: z in ( Bags {} ) by PRE_POLY:def 12;

          

           A11: (Py . z) = ((( Bags {} ) --> y) . z) by A2

          .= y by A10, FUNCOP_1: 7;

          

           A12: (Px . z) = ((( Bags {} ) --> x) . z) by A2

          .= x by A10, FUNCOP_1: 7;

          (Pxy . z) = ((( Bags {} ) --> (x + y)) . z) by A2

          .= (x + y) by A10, FUNCOP_1: 7;

          hence (Pxy . z) = ((Px . z) + (Py . z)) by A12, A11;

        end;

        then Pxy = (Px + Py) by POLYNOM1: 16;

        hence ((P . x) + (P . y)) = (P . (x + y)) by POLYNOM1:def 11;

      end;

      then

       A13: P is additive;

      now

        let x,y be Element of R;

        reconsider Px = (P . x), Py = (P . y), Pxy = (P . (x * y)) as Polynomial of 0 , R by POLYNOM1:def 11;

        now

          reconsider s = <*(x * y)*> as FinSequence of the carrier of R;

          let b be bag of 0 ;

          take s;

          

           A14: b in ( Bags {} ) by PRE_POLY:def 12;

          

          thus (Pxy . b) = ((( Bags {} ) --> (x * y)) . b) by A2

          .= (x * y) by A14, FUNCOP_1: 7

          .= ( Sum s) by RLVECT_1: 44;

          

           A15: ( decomp b) = <* <* {} , {} *>*> by Th2;

          

           A16: ( len s) = 1 by FINSEQ_1: 39;

          hence ( len s) = ( len ( decomp b)) by A15, FINSEQ_1: 39;

          

           A17: ( len ( decomp b)) = 1 by A15, FINSEQ_1: 39;

          now

            set b1 = {} , b2 = {} ;

            let k be Element of NAT ;

            

             A18: b1 in ( Bags {} ) by PRE_POLY: 51, TARSKI:def 1;

            then

            reconsider b1, b2 as bag of 0 ;

            

             A19: (Px . b1) = ((( Bags {} ) --> x) . b1) by A2

            .= x by A18, FUNCOP_1: 7;

            

             A20: (Py . b2) = ((( Bags {} ) --> y) . b2) by A2

            .= y by A18, FUNCOP_1: 7;

            assume

             A21: k in ( dom s);

            then

             A22: 1 <= k & k <= 1 by A16, FINSEQ_3: 25;

            then

             A23: k = 1 by XXREAL_0: 1;

            take b1, b2;

            k in ( dom ( decomp b)) by A17, A22, FINSEQ_3: 25;

            

            hence (( decomp b) /. k) = (( decomp b) . 1) by A23, PARTFUN1:def 6

            .= <*b1, b2*> by A15, FINSEQ_1: 40;

            

            thus (s /. k) = (s . 1) by A21, A23, PARTFUN1:def 6

            .= ((Px . b1) * (Py . b2)) by A19, A20, FINSEQ_1: 40;

          end;

          hence for k be Element of NAT st k in ( dom s) holds ex b1,b2 be bag of 0 st (( decomp b) /. k) = <*b1, b2*> & (s /. k) = ((Px . b1) * (Py . b2));

        end;

        then Pxy = (Px *' Py) by POLYNOM1:def 10;

        hence ((P . x) * (P . y)) = (P . (x * y)) by POLYNOM1:def 11;

      end;

      then

       A24: P is multiplicative;

      take P;

      reconsider f0 = ( { {} } --> ( 0. R)), f1 = ( { {} } --> ( 1_ R)) as Function of { {} }, the carrier of R;

      

       A25: ( dom f1) = { {} };

      

       A26: ( dom f0) = { {} };

      

       A27: {} in ( dom ( { {} } --> ( 0. R))) by TARSKI:def 1;

      ( 1_ ( Polynom-Ring ( 0 ,R))) = ( 1_ ( 0 ,R)) by POLYNOM1: 31

      .= (( 0_ ( 0 ,R)) +* ( {} ,( 1_ R))) by A9, POLYNOM1:def 9

      .= (( { {} } --> ( 0. R)) +* ( {} ,( 1_ R))) by POLYNOM1:def 8, PRE_POLY: 51

      .= (( { {} } --> ( 0. R)) +* ( {} .--> ( 1_ R))) by A27, FUNCT_7:def 3

      .= ( { {} } --> ( 1_ R)) by A26, A25, FUNCT_4: 19

      .= (P . ( 1_ R)) by A2, PRE_POLY: 51;

      then P is unity-preserving by GROUP_1:def 13;

      then

       A28: P is RingHomomorphism by A13, A24;

      then

       A29: P is RingEpimorphism by A8;

      now

        let x1,x2 be object;

        assume that

         A30: x1 in ( dom P) and

         A31: x2 in ( dom P);

        assume (P . x1) = (P . x2);

        then (( Bags {} ) --> x1) = (P . x2) by A2, A30;

        then (( Bags {} ) --> x1) = (( Bags {} ) --> x2) by A2, A31;

        hence x1 = x2 by FUNCT_4: 6;

      end;

      then P is one-to-one by FUNCT_1:def 4;

      then P is RingMonomorphism by A28;

      hence thesis by A29;

    end;

    theorem :: HILBASIS:29

    

     Th29: for R be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, n be Nat, b be bag of n, p1 be Polynomial of n, R, F be FinSequence of the carrier of ( Polynom-Ring (n,R)) st p1 = ( Sum F) holds ex g be Function of the carrier of ( Polynom-Ring (n,R)), the carrier of R st (for p be Polynomial of n, R holds (g . p) = (p . b)) & (p1 . b) = ( Sum (g * F))

    proof

      let R be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, n be Nat, b be bag of n, p1 be Polynomial of n, R, F be FinSequence of the carrier of ( Polynom-Ring (n,R));

      assume

       A1: p1 = ( Sum F);

      set CR = the carrier of R;

      set PNR = ( Polynom-Ring (n,R));

      set CPNR = the carrier of PNR;

      defpred P1[ Element of CPNR, Element of CR] means for p be Polynomial of n, R st p = $1 holds $2 = (p . b);

       A2:

      now

        let x be Element of CPNR;

        reconsider x9 = x as Polynomial of n, R by POLYNOM1:def 11;

         P1[x, (x9 . b)];

        hence ex y be Element of CR st P1[x, y];

      end;

      consider g be Function of CPNR, CR such that

       A3: for x be Element of CPNR holds P1[x, (g . x)] from FUNCT_2:sch 3( A2);

      take g;

      now

        let p be Polynomial of n, R;

        reconsider p9 = p as Element of CPNR by POLYNOM1:def 11;

         P1[p9, (g . p9)] by A3;

        hence (g . p) = (p . b);

      end;

      hence for p be Polynomial of n, R holds (g . p) = (p . b);

      defpred P2[ Nat] means for F9 be FinSequence of CPNR, p19 be Polynomial of n, R st ( len F9) <= $1 & p19 = ( Sum F9) holds (p19 . b) = ( Sum (g * F9));

      

       A4: for k be Nat st P2[k] holds P2[(k + 1)]

      proof

        let k be Nat;

        assume

         A5: P2[k];

        now

          let F9 be FinSequence of CPNR, p19 be Polynomial of n, R;

          assume that

           A6: ( len F9) <= (k + 1) and

           A7: p19 = ( Sum F9);

          per cases ;

            suppose ( len F9) < (k + 1);

            then ( len F9) <= k by NAT_1: 13;

            hence (p19 . b) = ( Sum (g * F9)) by A5, A7;

          end;

            suppose ( len F9) >= (k + 1);

            then ( len F9) = (k + 1) by A6, XXREAL_0: 1;

            then

            consider p,q be FinSequence such that

             A8: ( len p) = k and

             A9: ( len q) = 1 and

             A10: F9 = (p ^ q) by FINSEQ_2: 22;

            ( rng q) c= ( rng F9) by A10, FINSEQ_1: 30;

            then ( rng q) c= CPNR by XBOOLE_1: 1;

            then

            reconsider q as FinSequence of CPNR by FINSEQ_1:def 4;

            ( rng p) c= ( rng F9) by A10, FINSEQ_1: 29;

            then ( rng p) c= CPNR by XBOOLE_1: 1;

            then

            reconsider p as FinSequence of CPNR by FINSEQ_1:def 4;

            

             A11: ( Sum F9) = (( Sum p) + ( Sum q)) by A10, RLVECT_1: 41;

            reconsider p9 = ( Sum p) as Polynomial of n, R by POLYNOM1:def 11;

            

             A12: (g * F9) = ((g * p) ^ (g * q)) by A10, FINSEQOP: 9;

            1 in ( dom q) by A9, FINSEQ_3: 25;

            then (q . 1) in ( rng q) by FUNCT_1:def 3;

            then

            reconsider q9 = (q . 1) as Element of CPNR;

            reconsider q99 = q9 as Polynomial of n, R by POLYNOM1:def 11;

            

             A13: q = <*q9*> by A9, FINSEQ_1: 40;

            

            then (g * q) = <*(g . q9)*> by FINSEQ_2: 35

            .= <*(q99 . b)*> by A3;

            then

             A14: ( Sum (g * q)) = (q99 . b) by RLVECT_1: 44;

            q9 = ( Sum q) by A13, RLVECT_1: 44;

            then

             A15: p19 = (p9 + q99) by A7, A11, POLYNOM1:def 11;

            (p9 . b) = ( Sum (g * p)) by A5, A8;

            

            hence (p19 . b) = (( Sum (g * p)) + ( Sum (g * q))) by A14, A15, POLYNOM1: 15

            .= ( Sum (g * F9)) by A12, RLVECT_1: 41;

          end;

        end;

        hence thesis;

      end;

      

       A16: P2[ 0 ]

      proof

        let F9 be FinSequence of CPNR, p19 be Polynomial of n, R;

        assume that

         A17: ( len F9) <= 0 and

         A18: p19 = ( Sum F9);

        

         A19: F9 = ( <*> CPNR) by A17;

        then (g * F9) = ( <*> CR);

        then

         A20: ( Sum (g * F9)) = ( 0. R) by RLVECT_1: 43;

        p19 = ( 0. PNR) by A18, A19, RLVECT_1: 43

        .= ( 0_ (n,R)) by POLYNOM1:def 11;

        hence thesis by A20, POLYNOM1: 22;

      end;

      for k be Nat holds P2[k] from NAT_1:sch 2( A16, A4);

      then P2[( len F)];

      hence thesis by A1;

    end;

    definition

      let R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial doubleLoopStr, n be Nat;

      :: HILBASIS:def6

      func upm (n,R) -> Function of ( Polynom-Ring ( Polynom-Ring (n,R))), ( Polynom-Ring ((n + 1),R)) means

      : Def6: for p1 be Polynomial of ( Polynom-Ring (n,R)), p2 be Polynomial of n, R, p3 be Polynomial of (n + 1), R, b be bag of (n + 1) st p3 = (it . p1) & p2 = (p1 . (b . n)) holds (p3 . b) = (p2 . (b | n));

      existence

      proof

        set CR = the carrier of R;

        set PNR = ( Polynom-Ring (n,R));

        set PN1R = ( Polynom-Ring ((n + 1),R));

        set PRPNR = ( Polynom-Ring ( Polynom-Ring (n,R)));

        set CPRPNR = the carrier of PRPNR;

        set CPN1R = the carrier of PN1R;

        defpred P1[ Element of CPRPNR, Element of CPN1R] means for p1 be Polynomial of PNR, p2 be Polynomial of n, R, p3 be Polynomial of (n + 1), R, b be bag of (n + 1) st p1 = $1 & p3 = $2 & p2 = (p1 . (b . n)) holds (p3 . b) = (p2 . (b | n));

         A1:

        now

          let x be Element of CPRPNR;

          reconsider p1 = x as Polynomial of PNR by POLYNOM3:def 10;

          defpred P2[ Element of ( Bags (n + 1)), Element of CR] means for p2 be Polynomial of n, R st p2 = (p1 . ($1 . n)) holds $2 = (p2 . ($1 | n));

          deffunc F( object) = { b where b be Element of ( Bags (n + 1)) : (b . n) = $1 & for p2 be Polynomial of n, R st p2 = (p1 . $1) holds (b | n) in ( Support p2) };

           A2:

          now

            let k be object;

            assume k in NAT ;

            set Ak = F(k);

            Ak c= ( Bags (n + 1))

            proof

              let b be object;

              assume b in Ak;

              then ex b9 be Element of ( Bags (n + 1)) st b9 = b & (b9 . n) = k & for p2 be Polynomial of n, R st p2 = (p1 . k) holds (b9 | n) in ( Support p2);

              hence thesis;

            end;

            hence Ak in ( bool ( Bags (n + 1)));

          end;

          consider A be sequence of ( bool ( Bags (n + 1))) such that

           A3: for k be object st k in NAT holds (A . k) = F(k) from FUNCT_2:sch 2( A2);

          now

            let X be set;

            assume X in (A .: ( len p1));

            then

            consider k be Element of NAT such that k in ( len p1) and

             A4: X = (A . k) by FUNCT_2: 65;

            reconsider p2 = (p1 . k) as Polynomial of n, R by POLYNOM1:def 11;

            

             A5: (A . k) = { b where b be Element of ( Bags (n + 1)) : (b . n) = k & for p2 be Polynomial of n, R st p2 = (p1 . k) holds (b | n) in ( Support p2) } by A3;

            per cases ;

              suppose

               A6: ( Support p2) = {} ;

              now

                assume (A . k) <> {} ;

                then

                consider b be object such that

                 A7: b in (A . k) by XBOOLE_0:def 1;

                ex b9 be Element of ( Bags (n + 1)) st b9 = b & (b9 . n) = k & for p2 be Polynomial of n, R st p2 = (p1 . k) holds (b9 | n) in ( Support p2) by A5, A7;

                hence contradiction by A6;

              end;

              hence X is finite by A4;

            end;

              suppose

               A8: ( Support p2) <> {} ;

              then

              consider b2 be object such that

               A9: b2 in ( Support p2) by XBOOLE_0:def 1;

              reconsider b2 as Element of ( Bags n) by A9;

              

               A10: ((b2 bag_extend k) . n) = k by Def1;

              for p2 be Polynomial of n, R st p2 = (p1 . k) holds ((b2 bag_extend k) | n) in ( Support p2) by A9, Def1;

              then (b2 bag_extend k) in (A . k) by A5, A10;

              then

              reconsider Ak = (A . k) as non empty set;

              reconsider Supportp2 = ( Support p2) as non empty set by A8;

              defpred P3[ Element of Ak, Element of Supportp2] means for b be Element of ( Bags (n + 1)) st $1 = b holds $2 = (b | n);

               A11:

              now

                let x be Element of Ak;

                x in (A . k);

                then

                consider b be Element of ( Bags (n + 1)) such that

                 A12: b = x and (b . n) = k and

                 A13: for p2 be Polynomial of n, R st p2 = (p1 . k) holds (b | n) in ( Support p2) by A5;

                reconsider bn = (b | n) as Element of Supportp2 by A13;

                 P3[x, bn] by A12;

                hence ex y be Element of Supportp2 st P3[x, y];

              end;

              consider f be Function of Ak, Supportp2 such that

               A14: for x be Element of Ak holds P3[x, (f . x)] from FUNCT_2:sch 3( A11);

              

               A15: ( dom f) = Ak by FUNCT_2:def 1;

              now

                let x1,x2 be object;

                assume that

                 A16: x1 in ( dom f) and

                 A17: x2 in ( dom f) and

                 A18: (f . x1) = (f . x2);

                (f . x1) in Supportp2 by A16, FUNCT_2: 5;

                then

                reconsider fx1 = (f . x1) as Element of ( Bags n);

                consider b1 be Element of ( Bags (n + 1)) such that

                 A19: b1 = x1 and

                 A20: (b1 . n) = k and for p2 be Polynomial of n, R st p2 = (p1 . k) holds (b1 | n) in ( Support p2) by A5, A15, A16;

                (b1 | n) = (f . x1) by A14, A16, A19;

                then

                 A21: b1 = (fx1 bag_extend k) by A20, Def1;

                consider b2 be Element of ( Bags (n + 1)) such that

                 A22: b2 = x2 and

                 A23: (b2 . n) = k and for p2 be Polynomial of n, R st p2 = (p1 . k) holds (b2 | n) in ( Support p2) by A5, A15, A17;

                (b2 | n) = (f . x1) by A14, A17, A18, A22;

                hence x1 = x2 by A19, A21, A22, A23, Def1;

              end;

              then

               A24: f is one-to-one by FUNCT_1:def 4;

              ( rng f) c= Supportp2;

              then ( card Ak) c= ( card Supportp2) by A15, A24, CARD_1: 10;

              hence X is finite by A4;

            end;

          end;

          then

           A25: ( union (A .: ( len p1))) is finite by FINSET_1: 7;

           A26:

          now

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

            reconsider p2 = (p1 . (b . n)) as Polynomial of n, R by POLYNOM1:def 11;

            n < (n + 1) by XREAL_1: 29;

            then

            reconsider bn = (b | n) as bag of n by Th3;

             P2[b, (p2 . bn)];

            hence ex r be Element of CR st P2[b, r];

          end;

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

           A27: for b be Element of ( Bags (n + 1)) holds P2[b, (y . b)] from FUNCT_2:sch 3( A26);

          reconsider y as Function of ( Bags (n + 1)), R;

          reconsider y as Series of (n + 1), R;

          ( Support y) c= ( union (A .: ( len p1)))

          proof

            let x be object;

            

             A28: ( dom A) = NAT by FUNCT_2:def 1;

            assume

             A29: x in ( Support y);

            then

            reconsider x9 = x as Element of ( Bags (n + 1));

            reconsider p2 = (p1 . (x9 . n)) as Polynomial of n, R by POLYNOM1:def 11;

            n < (n + 1) by XREAL_1: 29;

            then

            reconsider xn = (x9 | n) as Element of ( Bags n) by Th3;

            (y . x9) <> ( 0. R) by A29, POLYNOM1:def 4;

            then

             A30: (p2 . xn) <> ( 0. R) by A27;

            then p2 <> ( 0_ (n,R)) by POLYNOM1: 22;

            then p2 <> ( 0. PNR) by POLYNOM1:def 11;

            then

             A31: (x9 . n) < ( len p1) by ALGSEQ_1: 8;

            ( len p1) = { i where i be Nat : i < ( len p1) } by AXIOMS: 4;

            then (x9 . n) in ( len p1) by A31;

            then

             A32: (A . (x9 . n)) in (A .: ( len p1)) by A28, FUNCT_1:def 6;

            

             A33: (A . (x9 . n)) = { b where b be Element of ( Bags (n + 1)) : (b . n) = (x9 . n) & for p2 be Polynomial of n, R st p2 = (p1 . (x9 . n)) holds (b | n) in ( Support p2) } by A3;

            for p2 be Polynomial of n, R st p2 = (p1 . (x9 . n)) holds xn in ( Support p2) by A30, POLYNOM1:def 4;

            then x in (A . (x9 . n)) by A33;

            hence thesis by A32, TARSKI:def 4;

          end;

          then y is finite-Support by A25, POLYNOM1:def 5;

          then

          reconsider y9 = y as Element of CPN1R by POLYNOM1:def 11;

          now

            let p1 be Polynomial of PNR, p2 be Polynomial of n, R, p3 be Polynomial of (n + 1), R, b be bag of (n + 1);

            

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

            assume p1 = x & p3 = y9 & p2 = (p1 . (b . n));

            hence (p3 . b) = (p2 . (b | n)) by A27, A34;

          end;

          hence ex y be Element of CPN1R st P1[x, y];

        end;

        consider P be Function of CPRPNR, CPN1R such that

         A35: for x be Element of CPRPNR holds P1[x, (P . x)] from FUNCT_2:sch 3( A1);

        reconsider P as Function of PRPNR, PN1R;

        take P;

        now

          let p1 be Polynomial of ( Polynom-Ring (n,R)), p2 be Polynomial of n, R, p3 be Polynomial of (n + 1), R, b be bag of (n + 1);

          

           A36: p1 in CPRPNR by POLYNOM3:def 10;

          assume p3 = (P . p1) & p2 = (p1 . (b . n));

          hence (p3 . b) = (p2 . (b | n)) by A35, A36;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let A,B be Function of ( Polynom-Ring ( Polynom-Ring (n,R))), ( Polynom-Ring ((n + 1),R));

        set CPN1R = the carrier of ( Polynom-Ring ((n + 1),R));

        set CPRPNR = the carrier of ( Polynom-Ring ( Polynom-Ring (n,R)));

        set PNR = ( Polynom-Ring (n,R));

        assume

         A37: for p1 be Polynomial of ( Polynom-Ring (n,R)), p2 be Polynomial of n, R, p3 be Polynomial of (n + 1), R, b be bag of (n + 1) st p3 = (A . p1) & p2 = (p1 . (b . n)) holds (p3 . b) = (p2 . (b | n));

        assume

         A38: for p1 be Polynomial of ( Polynom-Ring (n,R)), p2 be Polynomial of n, R, p3 be Polynomial of (n + 1), R, b be bag of (n + 1) st p3 = (B . p1) & p2 = (p1 . (b . n)) holds (p3 . b) = (p2 . (b | n));

        now

          let x be object;

          assume

           A39: x in CPRPNR;

          then

          reconsider x9 = x as Polynomial of PNR by POLYNOM3:def 10;

          (A . x) in CPN1R & (B . x) in CPN1R by A39, FUNCT_2: 5;

          then

          reconsider Ax = (A . x), Bx = (B . x) as Polynomial of (n + 1), R by POLYNOM1:def 11;

          now

            let b be object;

            assume b in ( Bags (n + 1));

            then

            reconsider b9 = b as Element of ( Bags (n + 1));

            reconsider p2 = (x9 . (b9 . n)) as Polynomial of n, R by POLYNOM1:def 11;

            n < (n + 1) by NAT_1: 13;

            then

            reconsider bn = (b9 | n) as Element of ( Bags n) by Th3;

            

            thus (Ax . b) = (p2 . bn) by A37

            .= (Bx . b) by A38;

          end;

          hence (A . x) = (B . x) by FUNCT_2: 12;

        end;

        hence A = B;

      end;

    end

    registration

      let R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial doubleLoopStr, n be Nat;

      cluster ( upm (n,R)) -> additive;

      coherence

      proof

        set P = ( upm (n,R));

        set PNR = ( Polynom-Ring (n,R));

        thus P is additive

        proof

          let x,y be Element of ( Polynom-Ring ( Polynom-Ring (n,R)));

          reconsider x9 = x, y9 = y, xy9 = (x + y) as Polynomial of PNR by POLYNOM3:def 10;

          reconsider Pxy = (P . (x + y)), Px = (P . x), Py = (P . y) as Polynomial of (n + 1), R by POLYNOM1:def 11;

          

           A1: xy9 = (x9 + y9) by POLYNOM3:def 10;

          now

            let b be object;

            assume b in ( Bags (n + 1));

            then

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

            reconsider xybn = ((x9 + y9) . (b9 . n)) as Polynomial of n, R by POLYNOM1:def 11;

            reconsider xbn = (x9 . (b9 . n)), ybn = (y9 . (b9 . n)) as Polynomial of n, R by POLYNOM1:def 11;

            n < (n + 1) by XREAL_1: 29;

            then

            reconsider bn = (b9 | n) as bag of n by Th3;

            

             A2: (xbn . bn) = (Px . b9) & (ybn . bn) = (Py . b9) by Def6;

            ((x9 + y9) . (b9 . n)) = ((x9 . (b9 . n)) + (y9 . (b9 . n))) by NORMSP_1:def 2;

            then xybn = (xbn + ybn) by POLYNOM1:def 11;

            

            hence (Pxy . b) = ((xbn + ybn) . bn) by A1, Def6

            .= ((Px . b9) + (Py . b9)) by A2, POLYNOM1: 15

            .= ((Px + Py) . b) by POLYNOM1: 15;

          end;

          

          hence (P . (x + y)) = (Px + Py) by FUNCT_2: 12

          .= ((P . x) + (P . y)) by POLYNOM1:def 11;

        end;

      end;

      cluster ( upm (n,R)) -> multiplicative;

      coherence

      proof

        set P = ( upm (n,R));

        set CR = the carrier of R;

        set PNR = ( Polynom-Ring (n,R));

        set CPNR = the carrier of PNR;

        thus P is multiplicative

        proof

          let x9,y9 be Element of the carrier of ( Polynom-Ring ( Polynom-Ring (n,R)));

          reconsider x = x9, y = y9, xy = (x9 * y9) as Polynomial of PNR by POLYNOM3:def 10;

          reconsider Pxy = (P . (x9 * y9)), PxPy = ((P . x9) * (P . y9)), Px = (P . x9), Py = (P . y9) as Polynomial of (n + 1), R by POLYNOM1:def 11;

          

           A3: xy = (x *' y) by POLYNOM3:def 10;

          

           A4: PxPy = (Px *' Py) by POLYNOM1:def 11;

          now

            let b9 be object;

            assume b9 in ( Bags (n + 1));

            then

            reconsider b = b9 as Element of ( Bags (n + 1));

            consider r be FinSequence of CPNR such that

             A5: ( len r) = ((b . n) + 1) and

             A6: (xy . (b . n)) = ( Sum r) and

             A7: for k be Element of NAT st k in ( dom r) holds (r . k) = ((x . (k -' 1)) * (y . (((b . n) + 1) -' k))) by A3, POLYNOM3:def 9;

            n < (n + 1) by NAT_1: 13;

            then

            reconsider bn = (b | n) as Element of ( Bags n) by Th3;

            defpred P3[ object, object] means for p,q be Polynomial of n, R, fcr be FinSequence of CR, i be Element of NAT st i = $1 & p = (x . (i -' 1)) & q = (y . (((b . n) + 1) -' i)) & fcr = $2 holds ((p *' q) . bn) = ( Sum fcr) & ( len fcr) = ( len ( decomp bn)) & for k be Element of NAT st k in ( dom fcr) holds ex b1,b2 be bag of n st (( decomp bn) /. k) = <*b1, b2*> & (fcr /. k) = ((p . b1) * (q . b2));

            reconsider xybn = (xy . (b . n)) as Polynomial of n, R by POLYNOM1:def 11;

            consider u be FinSequence of CR such that

             A8: (PxPy . b) = ( Sum u) and

             A9: ( len u) = ( len ( decomp b)) and

             A10: for k be Element of NAT st k in ( dom u) holds ex b1,b2 be bag of (n + 1) st (( decomp b) /. k) = <*b1, b2*> & (u /. k) = ((Px . b1) * (Py . b2)) by A4, POLYNOM1:def 10;

             A11:

            now

              let e9 be object;

              assume e9 in ( dom r);

              then

              reconsider e = e9 as Element of NAT ;

              reconsider p = (x . (e -' 1)), q = (y . (((b . n) + 1) -' e)) as Polynomial of n, R by POLYNOM1:def 11;

              consider fcr be FinSequence of CR such that

               A12: ((p *' q) . bn) = ( Sum fcr) & ( len fcr) = ( len ( decomp bn)) & for k be Element of NAT st k in ( dom fcr) holds ex b1,b2 be bag of n st (( decomp bn) /. k) = <*b1, b2*> & (fcr /. k) = ((p . b1) * (q . b2)) by POLYNOM1:def 10;

              

               A13: fcr in (CR * ) by FINSEQ_1:def 11;

               P3[e, fcr] by A12;

              hence ex u be object st u in (CR * ) & P3[e9, u] by A13;

            end;

            consider s be Function of ( dom r), (CR * ) such that

             A14: for e be object st e in ( dom r) holds P3[e, (s . e)] from FUNCT_2:sch 1( A11);

            

             A15: ( rng s) c= (CR * );

            

             A16: ( dom s) = ( dom r) by FUNCT_2:def 1;

            then ex n be Nat st ( dom s) = ( Seg n) by FINSEQ_1:def 2;

            then s is FinSequence-like by FINSEQ_1:def 2;

            then

            reconsider s as FinSequence of (CR * ) by A15, FINSEQ_1:def 4;

            consider g be Function of CPNR, CR such that

             A17: for p be Polynomial of n, R holds (g . p) = (p . bn) and

             A18: (xybn . bn) = ( Sum (g * r)) by A6, Th29;

            

             A19: ( Sum (g * r)) = (Pxy . b) by A18, Def6;

            ( 0 + 1) <= ( len r) by A5, XREAL_1: 6;

            then

             A20: 1 in ( dom s) by A16, FINSEQ_3: 25;

             A21:

            now

              reconsider p9 = (x . (1 -' 1)), q9 = (y . (((b . n) + 1) -' 1)) as Polynomial of n, R by POLYNOM1:def 11;

              (s /. 1) is FinSequence of CR;

              then

               A22: (s . 1) is FinSequence of CR by A20, PARTFUN1:def 6;

              p9 = (x . (1 -' 1)) & q9 = (y . (((b . n) + 1) -' 1));

              hence ( len (s . 1)) <> 0 by A14, A16, A20, A22;

            end;

            defpred P1[ object, object] means for i,n1 be Element of NAT , b1 be bag of (n + 1) st n1 = $1 & b1 = (( divisors b) . n1) & i in ( dom ( divisors bn)) & (( divisors bn) . i) = (b1 | n) holds ((b1 . n) + 1) in ( dom s) & i in ( dom (s . ((b1 . n) + 1))) & $2 = (( Sum ( Card (s | (((b1 . n) + 1) -' 1)))) + i);

            set t = ( FlattenSeq s);

             A23:

            now

              let n19 be object;

              assume

               A24: n19 in ( dom u);

              then

              reconsider n1 = n19 as Element of NAT ;

              ( dom u) = ( dom ( decomp b)) by A9, FINSEQ_3: 29

              .= ( dom ( divisors b)) by PRE_POLY:def 17;

              then

               A25: (( divisors b) . n1) in ( rng ( divisors b)) by A24, FUNCT_1:def 3;

              then

              reconsider b1 = (( divisors b) . n1) as bag of (n + 1);

              

               A26: b1 divides b by A25, Th7;

              then (b1 . n) <= (b . n) by PRE_POLY:def 11;

              then

               A27: ((b1 . n) + 1) <= ((b . n) + 1) by XREAL_1: 6;

              n < (n + 1) by NAT_1: 13;

              then

              reconsider b1n = (b1 | n) as Element of ( Bags n) by Th3;

              reconsider p = (x . (((b1 . n) + 1) -' 1)), q = (y . (((b . n) + 1) -' ((b1 . n) + 1))) as Polynomial of n, R by POLYNOM1:def 11;

              

               A28: p = (x . (((b1 . n) + 1) -' 1)) & q = (y . (((b . n) + 1) -' ((b1 . n) + 1)));

              b1n divides bn by A26, Th4;

              then b1n in ( rng ( divisors bn)) by Th7;

              then

              consider i be object such that

               A29: i in ( dom ( divisors bn)) and

               A30: b1n = (( divisors bn) . i) by FUNCT_1:def 3;

              reconsider i as Element of NAT by A29;

              set n2 = (( Sum ( Card (s | (((b1 . n) + 1) -' 1)))) + i);

              

               A31: ((b1 . n) + 1) >= (1 + 0 ) by XREAL_1: 6;

              then

               A32: ((b1 . n) + 1) in ( dom s) by A5, A16, A27, FINSEQ_3: 25;

              then (s . ((b1 . n) + 1)) is Element of (CR * ) by A16, FUNCT_2: 5;

              then ( len (s . ((b1 . n) + 1))) = ( len ( decomp bn)) by A14, A16, A32, A28;

              

              then

               A33: ( dom (s . ((b1 . n) + 1))) = ( dom ( decomp bn)) by FINSEQ_3: 29

              .= ( dom ( divisors bn)) by PRE_POLY:def 17;

              then

               A34: n2 in ( dom t) by A29, A32, PRE_POLY: 30;

              for i9,n19 be Element of NAT , b19 be bag of (n + 1) st n19 = n1 & b19 = (( divisors b) . n19) & i9 in ( dom ( divisors bn)) & (( divisors bn) . i9) = (b19 | n) holds ((b19 . n) + 1) in ( dom s) & i9 in ( dom (s . ((b19 . n) + 1))) & n2 = (( Sum ( Card (s | (((b19 . n) + 1) -' 1)))) + i9) by A5, A16, A29, A30, A27, A31, A33, FINSEQ_3: 25, FUNCT_1:def 4;

              hence ex n29 be object st n29 in ( dom t) & P1[n19, n29] by A34;

            end;

            consider p be Function of ( dom u), ( dom t) such that

             A35: for x be object st x in ( dom u) holds P1[x, (p . x)] from FUNCT_2:sch 1( A23);

            1 in ( dom ( Card s)) by A20, CARD_3:def 2;

            then ( Sum ( Card s)) >= (( Card s) . 1) by POLYNOM3: 4;

            then ( Sum ( Card s)) > 0 by A20, A21, CARD_3:def 2;

            then ( len t) > 0 by PRE_POLY: 27;

            then

             A36: t <> {} ;

            then

             A37: ( dom p) = ( dom u) by FUNCT_2:def 1;

            now

              let n19,n29 be object;

              assume that

               A38: n19 in ( dom p) and

               A39: n29 in ( dom p) and

               A40: (p . n19) = (p . n29);

              ( dom p) = ( dom u) by A36, FUNCT_2:def 1;

              then

              reconsider n1 = n19, n2 = n29 as Element of NAT by A38, A39;

              

               A41: ( dom u) = ( dom ( decomp b)) by A9, FINSEQ_3: 29

              .= ( dom ( divisors b)) by PRE_POLY:def 17;

              then

               A42: (( divisors b) . n1) in ( rng ( divisors b)) by A38, FUNCT_1:def 3;

              then

              reconsider b1 = (( divisors b) . n1) as bag of (n + 1);

              

               A43: (( divisors b) . n2) in ( rng ( divisors b)) by A39, A41, FUNCT_1:def 3;

              then

              reconsider b2 = (( divisors b) . n2) as bag of (n + 1);

              n < (n + 1) by NAT_1: 13;

              then

              reconsider b1n = (b1 | n), b2n = (b2 | n) as Element of ( Bags n) by Th3;

              

               A44: (( Card s) | (((b1 . n) + 1) -' 1)) = ( Card (s | (((b1 . n) + 1) -' 1))) & (( Card s) | (((b2 . n) + 1) -' 1)) = ( Card (s | (((b2 . n) + 1) -' 1))) by POLYNOM3: 16;

              b2 divides b by A43, Th7;

              then b2n divides bn by Th4;

              then b2n in ( rng ( divisors bn)) by Th7;

              then

              consider i2 be object such that

               A45: i2 in ( dom ( divisors bn)) and

               A46: b2n = (( divisors bn) . i2) by FUNCT_1:def 3;

              reconsider i2 as Element of NAT by A45;

              

               A47: ((b2 . n) + 1) in ( dom s) & i2 in ( dom (s . ((b2 . n) + 1))) by A35, A39, A45, A46;

              b1 divides b by A42, Th7;

              then b1n divides bn by Th4;

              then b1n in ( rng ( divisors bn)) by Th7;

              then

              consider i1 be object such that

               A48: i1 in ( dom ( divisors bn)) and

               A49: b1n = (( divisors bn) . i1) by FUNCT_1:def 3;

              reconsider i1 as Element of NAT by A48;

              

               A50: (p . n1) = (( Sum ( Card (s | (((b1 . n) + 1) -' 1)))) + i1) by A35, A38, A48, A49;

              

               A51: (p . n2) = (( Sum ( Card (s | (((b2 . n) + 1) -' 1)))) + i2) by A35, A39, A45, A46;

              

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

              ((b1 . n) + 1) in ( dom s) & i1 in ( dom (s . ((b1 . n) + 1))) by A35, A38, A48, A49;

              then

               A53: ((b1 . n) + 1) = ((b2 . n) + 1) & i1 = i2 by A40, A50, A47, A51, A44, POLYNOM3: 22;

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

              

              then b1 = (b1n bag_extend (b1 . n)) by Def1

              .= b2 by A49, A46, A53, A52, Def1;

              hence n19 = n29 by A38, A39, A41, FUNCT_1:def 4;

            end;

            then

             A54: p is one-to-one by FUNCT_1:def 4;

            ( dom t) c= ( rng p)

            proof

              let n19 be object;

              assume

               A55: n19 in ( dom t);

              then

              reconsider n1 = n19 as Element of NAT ;

              consider i,j be Nat such that

               A56: i in ( dom s) and

               A57: j in ( dom (s . i)) and

               A58: n1 = (( Sum ( Card (s | (i -' 1)))) + j) and ((s . i) . j) = (t . n1) by A55, PRE_POLY: 29;

              (s . i) in (CR * ) by A16, A56, FUNCT_2: 5;

              then

               A59: (s . i) is FinSequence of CR by FINSEQ_1:def 11;

              reconsider bj = (( divisors bn) /. j) as bag of n;

              set bij = (bj bag_extend (i -' 1));

              reconsider p9 = (x . (i -' 1)), q9 = (y . (((b . n) + 1) -' i)) as Polynomial of n, R by POLYNOM1:def 11;

              

               A60: (bij . n) = (i -' 1) by Def1;

              1 <= i by A56, FINSEQ_3: 25;

              then

               A61: ((bij . n) + 1) = i by A60, XREAL_1: 235;

              

               A62: ( dom u) = ( dom ( decomp b)) by A9, FINSEQ_3: 29

              .= ( dom ( divisors b)) by PRE_POLY:def 17;

              p9 = (x . (i -' 1)) & q9 = (y . (((b . n) + 1) -' i));

              then ( len (s . i)) = ( len ( decomp bn)) by A14, A16, A56, A59;

              

              then

               A63: ( dom (s . i)) = ( dom ( decomp bn)) by FINSEQ_3: 29

              .= ( dom ( divisors bn)) by PRE_POLY:def 17;

              then

               A64: bj = (( divisors bn) . j) by A57, PARTFUN1:def 6;

              then bj in ( rng ( divisors bn)) by A57, A63, FUNCT_1:def 3;

              then

               A65: bj divides bn by Th7;

              now

                let k be object;

                per cases ;

                  suppose

                   A66: k in (n + 1);

                  now

                    per cases ;

                      suppose

                       A67: k in n;

                      then

                       A68: (b . k) = (bn . k) by FUNCT_1: 49;

                      (bij . k) = ((bij | n) . k) by A67, FUNCT_1: 49

                      .= (bj . k) by Def1;

                      hence (bij . k) <= (b . k) by A65, A68, PRE_POLY:def 11;

                    end;

                      suppose

                       A69: not k in n;

                      

                       A70: 1 <= i by A56, FINSEQ_3: 25;

                      i <= ((b . n) + 1) by A5, A16, A56, FINSEQ_3: 25;

                      then

                       A71: (i - 1) <= (((b . n) + 1) - 1) by XREAL_1: 9;

                      ( Segm (n + 1)) = (( Segm n) \/ {n}) by AFINSQ_1: 2;

                      then k in {n} by A66, A69, XBOOLE_0:def 3;

                      then

                       A72: k = n by TARSKI:def 1;

                      then (bij . k) = (i -' 1) by Def1;

                      hence (bij . k) <= (b . k) by A72, A70, A71, XREAL_1: 233;

                    end;

                  end;

                  hence (bij . k) <= (b . k);

                end;

                  suppose

                   A73: not k in (n + 1);

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

                  hence (bij . k) <= (b . k) by A73, FUNCT_1:def 2;

                end;

              end;

              then bij divides b by PRE_POLY:def 11;

              then bij in ( rng ( divisors b)) by Th7;

              then

              consider k be object such that

               A74: k in ( dom ( divisors b)) and

               A75: bij = (( divisors b) . k) by FUNCT_1:def 3;

              

               A76: ( dom p) = ( dom u) by A36, FUNCT_2:def 1;

              (( divisors bn) . j) = (bij | n) by A64, Def1;

              then (p . k) = (( Sum ( Card (s | (((bij . n) + 1) -' 1)))) + j) by A35, A57, A63, A74, A75, A62;

              hence thesis by A58, A74, A76, A62, A61, FUNCT_1:def 3;

            end;

            then

             A77: ( rng p) = ( dom t) by XBOOLE_0:def 10;

            ( len ( Sum s)) = ( len s) by MATRLIN:def 6;

            then

             A78: ( dom ( Sum s)) = ( dom r) by A16, FINSEQ_3: 29;

             A79:

            now

              let k be Nat;

              reconsider p = (x . (k -' 1)), q = (y . (((b . n) + 1) -' k)) as Polynomial of n, R by POLYNOM1:def 11;

              reconsider pq9 = (p *' q) as Element of CPNR by POLYNOM1:def 11;

              assume

               A80: k in ( dom r);

              then

              reconsider sk = (s . k) as Element of (CR * ) by FUNCT_2: 5;

              reconsider sk as FinSequence of CR;

              

               A81: (r . k) = ((x . (k -' 1)) * (y . (((b . n) + 1) -' k))) by A7, A80

              .= pq9 by POLYNOM1:def 11;

              (( Sum s) /. k) = (( Sum s) . k) & (s /. k) = (s . k) by A16, A78, A80, PARTFUN1:def 6;

              

              hence (( Sum s) . k) = ( Sum sk) by A78, A80, MATRLIN:def 6

              .= ((p *' q) . bn) by A14, A80

              .= (g . (r . k)) by A17, A81

              .= ((g * r) . k) by A80, FUNCT_1: 13;

            end;

             A82:

            now

              let n1 be Nat;

              reconsider b19 = (( divisors b) /. n1) as bag of (n + 1);

              assume

               A83: n1 in ( dom u);

              then

              consider b1,b2 be bag of (n + 1) such that

               A84: (( decomp b) /. n1) = <*b1, b2*> and

               A85: (u /. n1) = ((Px . b1) * (Py . b2)) by A10;

              

               A86: ( dom u) = ( dom ( decomp b)) by A9, FINSEQ_3: 29;

              then

               A87: <*b1, b2*> = <*b19, (b -' b19)*> by A83, A84, PRE_POLY:def 17;

              then

               A88: b1 = b19 by FINSEQ_1: 77;

              reconsider xb1n = (x . (b1 . n)), yb2n = (y . (b2 . n)) as Polynomial of n, R by POLYNOM1:def 11;

              n < (n + 1) by NAT_1: 13;

              then

              reconsider b1n = (b1 | n), b2n = (b2 | n) as Element of ( Bags n) by Th3;

              

               A89: (u . n1) = ((Px . b1) * (Py . b2)) by A83, A85, PARTFUN1:def 6

              .= ((xb1n . b1n) * (Py . b2)) by Def6

              .= ((xb1n . b1n) * (yb2n . b2n)) by Def6;

              

               A90: b2 = (b -' b19) by A87, FINSEQ_1: 77;

              

               A91: n1 in ( dom ( divisors b)) by A83, A86, PRE_POLY:def 17;

              then

               A92: b1 = (( divisors b) . n1) by A88, PARTFUN1:def 6;

              then b1 in ( rng ( divisors b)) by A91, FUNCT_1:def 3;

              then

               A93: b1 divides b by Th7;

              then b1n divides bn by Th4;

              then b1n in ( rng ( divisors bn)) by Th7;

              then

              consider i be object such that

               A94: i in ( dom ( divisors bn)) and

               A95: b1n = (( divisors bn) . i) by FUNCT_1:def 3;

              reconsider i as Element of NAT by A94;

              

               A96: (b1 . n) <= (b . n) by A93, PRE_POLY:def 11;

              then ((b1 . n) + 1) <= ((b . n) + 1) by XREAL_1: 6;

              

              then

               A97: (((b . n) + 1) -' ((b1 . n) + 1)) = (((b . n) + 1) - ((b1 . n) + 1)) by XREAL_1: 233

              .= ((((b . n) - (b1 . n)) + 1) - 1)

              .= ((b . n) -' (b1 . n)) by A96, XREAL_1: 233

              .= (b2 . n) by A88, A90, PRE_POLY:def 6;

              

               A98: (((b1 . n) + 1) -' 1) = (((b1 . n) + 1) - 1) by NAT_D: 37

              .= (b1 . n);

              then

               A99: xb1n = (x . (((b1 . n) + 1) -' 1));

              

               A100: ((b1 . n) + 1) in ( dom s) by A35, A83, A92, A94, A95;

              then (s . ((b1 . n) + 1)) is Element of (CR * ) by A16, FUNCT_2: 5;

              then

              reconsider sb1n1 = (s . ((b1 . n) + 1)) as FinSequence of CR;

              

               A101: i in ( dom (s . ((b1 . n) + 1))) by A35, A83, A92, A94, A95;

              then

              consider B1,B2 be bag of n such that

               A102: (( decomp bn) /. i) = <*B1, B2*> and

               A103: (sb1n1 /. i) = ((xb1n . B1) * (yb2n . B2)) by A14, A16, A100, A98, A97;

              (p . n1) = (( Sum ( Card (s | (((b1 . n) + 1) -' 1)))) + i) by A35, A83, A92, A94, A95;

              then

               A104: (t . (p . n1)) = ((s . ((b1 . n) + 1)) . i) by A100, A101, PRE_POLY: 30;

              reconsider B19 = (( divisors bn) /. i) as bag of n;

              

               A105: ( dom ( divisors bn)) = ( dom ( decomp bn)) by PRE_POLY:def 17;

              then

               A106: <*B1, B2*> = <*B19, (bn -' B19)*> by A94, A102, PRE_POLY:def 17;

              then

               A107: B1 = B19 by FINSEQ_1: 77;

              then

               A108: B1 = b1n by A94, A95, PARTFUN1:def 6;

              yb2n = (y . (((b . n) + 1) -' ((b1 . n) + 1))) by A97;

              then ( len sb1n1) = ( len ( decomp bn)) by A14, A16, A100, A99;

              then

               A109: ( dom sb1n1) = ( dom ( divisors bn)) by A105, FINSEQ_3: 29;

              B2 = (bn -' B19) by A106, FINSEQ_1: 77;

              then B2 = b2n by A88, A90, A107, A108, Th5;

              hence (u . n1) = (t . (p . n1)) by A89, A94, A104, A103, A108, A109, PARTFUN1:def 6;

            end;

            ( dom r) = ( dom (g * r)) by FINSEQ_3: 120;

            then ( Sum s) = (g * r) by A78, A79, FINSEQ_1: 13;

            then

             A110: ( Sum t) = (Pxy . b) by A19, POLYNOM1: 14;

            

             A111: ( len u) = ( card ( dom u)) by CARD_1: 62

            .= ( card p qua set) by A37, CARD_1: 62

            .= ( card ( dom t)) by A54, A77, PRE_POLY: 19

            .= ( len t) by CARD_1: 62;

            then

             A112: ( dom u) = ( dom t) by FINSEQ_3: 29;

            then p is Permutation of ( dom u) by A54, A77, FUNCT_2: 57;

            hence (Pxy . b9) = (PxPy . b9) by A110, A8, A82, A111, A112, RLVECT_2: 6;

          end;

          hence (P . (x9 * y9)) = ((P . x9) * (P . y9)) by FUNCT_2: 12;

        end;

      end;

      cluster ( upm (n,R)) -> unity-preserving;

      coherence

      proof

        set P = ( upm (n,R));

        set PNR = ( Polynom-Ring (n,R));

        set PN1R = ( Polynom-Ring ((n + 1),R));

        set PRPNR = ( Polynom-Ring ( Polynom-Ring (n,R)));

        set CPN1R = the carrier of PN1R;

        reconsider p1 = ( 1_ PRPNR) as Polynomial of PNR by POLYNOM3:def 10;

        reconsider p19 = ( 1_ PN1R) as Polynomial of (n + 1), R by POLYNOM1:def 11;

        (P . ( 1_ PRPNR)) in CPN1R;

        then

        reconsider p3 = (P . p1) as Polynomial of (n + 1), R by POLYNOM1:def 11;

        now

          let x be object;

          assume x in ( Bags (n + 1));

          then

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

          reconsider p2 = (p1 . (b . n)) as Polynomial of n, R by POLYNOM1:def 11;

          

           A113: (p3 . b) = (p2 . (b | n)) by Def6;

          now

            per cases ;

              suppose

               A114: (b | n) = ( EmptyBag n) & (b . n) = 0 ;

              

              then

               A115: b = (( EmptyBag n) bag_extend 0 ) by Def1

              .= ( EmptyBag (n + 1)) by Th6;

              p2 = (( 1_. PNR) . 0 ) by A114, POLYNOM3:def 10

              .= ( 1_ PNR) by POLYNOM3: 30

              .= ( 1_ (n,R)) by POLYNOM1: 31;

              

              hence (p3 . b) = ( 1_ R) by A113, A114, POLYNOM1: 25

              .= (( 1_ ((n + 1),R)) . b) by A115, POLYNOM1: 25

              .= (p19 . b) by POLYNOM1: 31;

            end;

              suppose

               A116: (b | n) <> ( EmptyBag n) or (b . n) <> 0 ;

               A117:

              now

                n < (n + 1) by NAT_1: 13;

                then

                 A118: (b | n) is bag of n by Th3;

                

                 A119: p2 = (( 1_. PNR) . (b . n)) by POLYNOM3:def 10;

                per cases ;

                  suppose

                   A120: (b . n) = 0 ;

                  

                  then p2 = ( 1_ PNR) by A119, POLYNOM3: 30

                  .= ( 1_ (n,R)) by POLYNOM1: 31;

                  hence (p3 . b) = ( 0. R) by A113, A116, A118, A120, POLYNOM1: 25;

                end;

                  suppose (b . n) <> 0 ;

                  

                  then p2 = ( 0. PNR) by A119, POLYNOM3: 30

                  .= ( 0_ (n,R)) by POLYNOM1:def 11;

                  hence (p3 . b) = ( 0. R) by A113, A118, POLYNOM1: 22;

                end;

              end;

              b <> (( EmptyBag n) bag_extend 0 ) by A116, Def1;

              then b <> ( EmptyBag (n + 1)) by Th6;

              

              hence (p3 . b) = (( 1_ ((n + 1),R)) . b) by A117, POLYNOM1: 25

              .= (p19 . b) by POLYNOM1: 31;

            end;

          end;

          hence (p3 . x) = (p19 . x);

        end;

        then p19 = p3;

        hence thesis by GROUP_1:def 13;

      end;

      cluster ( upm (n,R)) -> one-to-one;

      coherence

      proof

        set P = ( upm (n,R));

        set PNR = ( Polynom-Ring (n,R));

        set PRPNR = ( Polynom-Ring ( Polynom-Ring (n,R)));

        now

          let x9,y9 be Element of PRPNR;

          reconsider x = x9, y = y9 as Polynomial of PNR by POLYNOM3:def 10;

          reconsider Py = (P . y9) as Polynomial of (n + 1), R by POLYNOM1:def 11;

          assume

           A121: (P . x9) = (P . y9);

          now

            let bn9 be object;

            assume bn9 in NAT ;

            then

            reconsider bn = bn9 as Element of NAT ;

            reconsider xbn = (x . bn), ybn = (y . bn) as Polynomial of n, R by POLYNOM1:def 11;

            now

              let b9 be object;

              assume b9 in ( Bags n);

              then

              reconsider b = b9 as bag of n;

              set bn1 = (b bag_extend bn);

              

               A122: (bn1 | n) = b & (bn1 . n) = bn by Def1;

              

              then (xbn . b) = (Py . bn1) by A121, Def6

              .= (ybn . b) by A122, Def6;

              hence (xbn . b9) = (ybn . b9);

            end;

            hence (x . bn9) = (y . bn9) by FUNCT_2: 12;

          end;

          hence x9 = y9 by FUNCT_2: 12;

        end;

        hence thesis by WAYBEL_1:def 1;

      end;

    end

    definition

      let R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial doubleLoopStr, n be Nat;

      :: HILBASIS:def7

      func mpu (n,R) -> Function of ( Polynom-Ring ((n + 1),R)), ( Polynom-Ring ( Polynom-Ring (n,R))) means

      : Def7: for p1 be Polynomial of (n + 1), R, p2 be Polynomial of n, R, p3 be Polynomial of ( Polynom-Ring (n,R)), i be Element of NAT , b be bag of n st p3 = (it . p1) & p2 = (p3 . i) holds (p2 . b) = (p1 . (b bag_extend i));

      existence

      proof

        set CR = the carrier of R;

        set PNR = ( Polynom-Ring (n,R));

        set PN1R = ( Polynom-Ring ((n + 1),R));

        set PRPNR = ( Polynom-Ring ( Polynom-Ring (n,R)));

        set CPRPNR = the carrier of PRPNR;

        set CPN1R = the carrier of PN1R;

        set CPNR = the carrier of PNR;

        defpred P1[ Element of CPN1R, Element of CPRPNR] means for p1 be Polynomial of (n + 1), R, p2 be Polynomial of n, R, p3 be Polynomial of ( Polynom-Ring (n,R)), i be Element of NAT , b be bag of n st p1 = $1 & p3 = $2 & p2 = (p3 . i) holds (p2 . b) = (p1 . (b bag_extend i));

         A1:

        now

          let x be Element of CPN1R;

          reconsider p1 = x as Polynomial of (n + 1), R by POLYNOM1:def 11;

          defpred P2[ Element of NAT , Element of CPNR] means for p2 be Polynomial of n, R, b be bag of n st p2 = $2 holds (p2 . b) = (p1 . (b bag_extend $1));

           A2:

          now

            let i be Element of NAT ;

            deffunc F( Element of ( Bags n)) = (p1 . ($1 bag_extend i));

            consider p2 be Function of ( Bags n), CR such that

             A3: for b be Element of ( Bags n) holds (p2 . b) = F(b) from FUNCT_2:sch 4;

            reconsider p2 as Function of ( Bags n), R;

            reconsider p2 as Series of n, R;

            now

              per cases ;

                suppose

                 A4: ( Support p1) = {} ;

                now

                  assume ( Support p2) <> {} ;

                  then

                  consider b be object such that

                   A5: b in ( Support p2) by XBOOLE_0:def 1;

                  reconsider b as Element of ( Bags n) by A5;

                  (p2 . b) <> ( 0. R) by A5, POLYNOM1:def 4;

                  then (p1 . (b bag_extend i)) <> ( 0. R) by A3;

                  hence ( Support p1) <> {} by POLYNOM1:def 4;

                end;

                hence ( Support p2) is finite by A4;

              end;

                suppose ( Support p2) = {} ;

                hence ( Support p2) is finite;

              end;

                suppose

                 A6: ( Support p1) <> {} & ( Support p2) <> {} ;

                then

                reconsider Supportp2 = ( Support p2) as non empty Subset of ( Bags n);

                reconsider Supportp1 = ( Support p1) as non empty Subset of ( Bags (n + 1)) by A6;

                defpred P[ Element of Supportp2, set] means $2 = ($1 bag_extend i);

                 A7:

                now

                  let x be Element of Supportp2;

                  x is Element of ( Bags n) & (p2 . x) <> ( 0. R) by POLYNOM1:def 4;

                  then (p1 . (x bag_extend i)) <> ( 0. R) by A3;

                  then (x bag_extend i) in ( Support p1) by POLYNOM1:def 4;

                  hence ex y be Element of Supportp1 st P[x, y];

                end;

                consider f be Function of Supportp2, Supportp1 such that

                 A8: for x be Element of Supportp2 holds P[x, (f . x)] from FUNCT_2:sch 3( A7);

                

                 A9: ( dom f) = Supportp2 by FUNCT_2:def 1;

                now

                  let x1,x2 be object;

                  assume that

                   A10: x1 in ( dom f) and

                   A11: x2 in ( dom f) and

                   A12: (f . x1) = (f . x2);

                  reconsider x19 = x1, x29 = x2 as Element of ( Bags n) by A9, A10, A11;

                  

                   A13: (x19 bag_extend i) = (f . x1) by A8, A10

                  .= (x29 bag_extend i) by A8, A11, A12;

                  x19 = ((x19 bag_extend i) | n) by Def1

                  .= x29 by A13, Def1;

                  hence x1 = x2;

                end;

                then

                 A14: f is one-to-one by FUNCT_1:def 4;

                ( rng f) c= Supportp1;

                then ( card Supportp2) c= ( card Supportp1) by A9, A14, CARD_1: 10;

                hence ( Support p2) is finite;

              end;

            end;

            then p2 is finite-Support by POLYNOM1:def 5;

            then

            reconsider p29 = p2 as Element of CPNR by POLYNOM1:def 11;

            take p29;

            now

              let p299 be Polynomial of n, R, b be bag of n;

              

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

              assume p299 = p29;

              hence (p299 . b) = (p1 . (b bag_extend i)) by A3, A15;

            end;

            hence P2[i, p29];

          end;

          consider p3 be sequence of CPNR such that

           A16: for x be Element of NAT holds P2[x, (p3 . x)] from FUNCT_2:sch 3( A2);

          reconsider p3 as sequence of PNR;

          now

            per cases ;

              suppose

               A17: ( Support p1) = {} ;

              now

                let i be Nat;

                assume i >= 0 ;

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

                reconsider p2 = (p3 . i1) as Polynomial of n, R by POLYNOM1:def 11;

                 A18:

                now

                  let x be object;

                  assume x in ( Bags n);

                  then

                  reconsider x9 = x as Element of ( Bags n);

                  (p1 . (x9 bag_extend i)) = ( 0. R) by A17, POLYNOM1:def 4;

                  then (p2 . x9) = ( 0. R) by A16;

                  hence (p2 . x) = ((( Bags n) --> ( 0. R)) . x);

                end;

                p2 = (( Bags n) --> ( 0. R)) by A18;

                

                hence (p3 . i) = ( 0_ (n,R)) by POLYNOM1:def 8

                .= ( 0. PNR) by POLYNOM1:def 11;

              end;

              hence p3 is finite-Support by ALGSEQ_1:def 1;

            end;

              suppose ( Support p1) <> {} ;

              then

              reconsider Supportp1 = ( Support p1) as finite non empty Subset of ( Bags (n + 1));

              deffunc F( Element of ( Bags (n + 1))) = ($1 . n);

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

               A19: for x be Element of ( Bags (n + 1)) holds (f . x) = F(x) from FUNCT_2:sch 4;

              reconsider j = ( max (f .: Supportp1)) as Element of NAT by ORDINAL1:def 12;

              now

                let i be Nat;

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

                reconsider p2 = (p3 . i1) as Polynomial of n, R by POLYNOM1:def 11;

                assume

                 A20: i >= (j + 1);

                 A21:

                now

                  let x be object;

                  assume x in ( Bags n);

                  then

                  reconsider x9 = x as Element of ( Bags n);

                  i > j by A20, NAT_1: 13;

                  then

                   A22: not i in (f .: Supportp1) by XXREAL_2:def 8;

                  (f . (x9 bag_extend i)) = ((x9 bag_extend i) . n) by A19

                  .= i by Def1;

                  then not (x9 bag_extend i) in Supportp1 by A22, FUNCT_2: 35;

                  then (p1 . (x9 bag_extend i)) = ( 0. R) by POLYNOM1:def 4;

                  then (p2 . x9) = ( 0. R) by A16;

                  hence (p2 . x) = ((( Bags n) --> ( 0. R)) . x);

                end;

                p2 = (( Bags n) --> ( 0. R)) by A21;

                

                hence (p3 . i) = ( 0_ (n,R)) by POLYNOM1:def 8

                .= ( 0. PNR) by POLYNOM1:def 11;

              end;

              hence p3 is finite-Support by ALGSEQ_1:def 1;

            end;

          end;

          then

          reconsider y = p3 as Element of CPRPNR by POLYNOM3:def 10;

          take y;

          thus P1[x, y] by A16;

        end;

        consider P be Function of CPN1R, CPRPNR such that

         A23: for x be Element of CPN1R holds P1[x, (P . x)] from FUNCT_2:sch 3( A1);

        reconsider P as Function of PN1R, PRPNR;

        take P;

        now

          let p1 be Polynomial of (n + 1), R, p2 be Polynomial of n, R, p3 be Polynomial of ( Polynom-Ring (n,R)), i be Element of NAT , b be bag of n;

          

           A24: p1 in CPN1R by POLYNOM1:def 11;

          assume p3 = (P . p1) & p2 = (p3 . i);

          hence (p2 . b) = (p1 . (b bag_extend i)) by A23, A24;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set PNR = ( Polynom-Ring (n,R));

        set PN1R = ( Polynom-Ring ((n + 1),R));

        set PRPNR = ( Polynom-Ring ( Polynom-Ring (n,R)));

        set CPN1R = the carrier of PN1R;

        let A,B be Function of PN1R, PRPNR;

        assume

         A25: for p1 be Polynomial of (n + 1), R, p2 be Polynomial of n, R, p3 be Polynomial of ( Polynom-Ring (n,R)), i be Element of NAT , b be bag of n st p3 = (A . p1) & p2 = (p3 . i) holds (p2 . b) = (p1 . (b bag_extend i));

        assume

         A26: for p1 be Polynomial of (n + 1), R, p2 be Polynomial of n, R, p3 be Polynomial of ( Polynom-Ring (n,R)), i be Element of NAT , b be bag of n st p3 = (B . p1) & p2 = (p3 . i) holds (p2 . b) = (p1 . (b bag_extend i));

        now

          let x be object;

          assume

           A27: x in CPN1R;

          then

          reconsider x99 = x as Element of CPN1R;

          reconsider x9 = x as Polynomial of (n + 1), R by A27, POLYNOM1:def 11;

          reconsider Ax = (A . x99), Bx = (B . x99) as Polynomial of PNR by POLYNOM3:def 10;

          now

            let i be object;

            assume i in NAT ;

            then

            reconsider i9 = i as Element of NAT ;

            reconsider Axi = (Ax . i9), Bxi = (Bx . i9) as Polynomial of n, R by POLYNOM1:def 11;

            now

              let b be object;

              assume b in ( Bags n);

              then

              reconsider b9 = b as bag of n;

              

              thus (Axi . b) = (x9 . (b9 bag_extend i9)) by A25

              .= (Bxi . b) by A26;

            end;

            hence (Ax . i) = (Bx . i) by FUNCT_2: 12;

          end;

          hence (A . x) = (B . x) by FUNCT_2: 12;

        end;

        hence A = B;

      end;

    end

    theorem :: HILBASIS:30

    

     Th30: for R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial non empty doubleLoopStr, n be Nat, p be Element of ( Polynom-Ring ((n + 1),R)) holds (( upm (n,R)) . (( mpu (n,R)) . p)) = p

    proof

      let R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial doubleLoopStr, n be Nat, p be Element of ( Polynom-Ring ((n + 1),R));

      set PNR = ( Polynom-Ring (n,R));

      reconsider p9 = p as Polynomial of (n + 1), R by POLYNOM1:def 11;

      reconsider upmmpup = (( upm (n,R)) . (( mpu (n,R)) . p)) as Polynomial of (n + 1), R by POLYNOM1:def 11;

      reconsider mpup = (( mpu (n,R)) . p) as Polynomial of PNR by POLYNOM3:def 10;

      now

        let b9 be object;

        assume b9 in ( Bags (n + 1));

        then

        reconsider b = b9 as Element of ( Bags (n + 1));

        reconsider mpupbn = (mpup . (b . n)) as Polynomial of n, R by POLYNOM1:def 11;

        n < (n + 1) by NAT_1: 13;

        then

        reconsider bn = (b | n) as bag of n by Th3;

        

         A1: b = (bn bag_extend (b . n)) by Def1;

        

        thus (upmmpup . b9) = (mpupbn . bn) by Def6

        .= (p9 . b9) by A1, Def7;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: HILBASIS:31

    

     Th31: for R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial non empty doubleLoopStr, n be Nat holds ex P be Function of ( Polynom-Ring ( Polynom-Ring (n,R))), ( Polynom-Ring ((n + 1),R)) st P is RingIsomorphism

    proof

      let R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial doubleLoopStr, n be Nat;

      set PN1R = ( Polynom-Ring ((n + 1),R));

      set CPRPNR = the carrier of ( Polynom-Ring ( Polynom-Ring (n,R)));

      set CPN1R = the carrier of PN1R;

      set P = ( upm (n,R));

      now

        let p be object;

        assume p in CPN1R;

        then

        reconsider p9 = p as Element of CPN1R;

        ( dom P) = CPRPNR & (P . (( mpu (n,R)) . p9)) = p9 by Th30, FUNCT_2:def 1;

        hence p in ( rng P) by FUNCT_1:def 3;

      end;

      then CPN1R c= ( rng P);

      then ( rng P) = CPN1R by XBOOLE_0:def 10;

      then P is onto;

      then P is RingEpimorphism;

      then P is RingIsomorphism;

      hence thesis;

    end;

    begin

    registration

      let R be Noetherian Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non empty doubleLoopStr;

      ::$Notion-Name

      cluster ( Polynom-Ring R) -> Noetherian;

      coherence

      proof

        set cR = the carrier of R;

        set PR = ( Polynom-Ring R);

        set cPR = the carrier of PR;

        now

          assume PR is non Noetherian;

          then

          consider I be Ideal of PR such that

           A1: I is non finitely_generated;

          defpred P1[ set, set, set] means ($2 is non empty finite Subset of I) implies (ex A,B be non empty Subset of cPR st A = $2 & B = (I \ (A -Ideal )) & ex r be Element of cPR st r in ( minlen B) & $3 = ($2 \/ {r}));

           A2:

          now

            let n be Nat, x be Subset of cPR;

            per cases ;

              suppose not x is non empty finite Subset of I;

              hence ex y be Subset of cPR st P1[n, x, y];

            end;

              suppose

               A3: x is non empty finite Subset of I;

              then

              reconsider x9 = x as non empty Subset of cPR;

              set B = (I \ (x9 -Ideal ));

              now

                assume B = {} ;

                then

                 A4: I c= (x9 -Ideal ) by XBOOLE_1: 37;

                (x9 -Ideal ) c= (I -Ideal ) by A3, IDEAL_1: 57;

                then (x9 -Ideal ) c= I by IDEAL_1: 44;

                hence contradiction by A1, A3, A4, XBOOLE_0:def 10;

              end;

              then

              reconsider B as non empty Subset of cPR;

              consider r be object such that

               A5: r in ( minlen B) by XBOOLE_0:def 1;

              ( minlen B) c= cPR by XBOOLE_1: 1;

              then

              reconsider r as Element of cPR by A5;

               P1[n, x, (x9 \/ {r})] by A5;

              hence ex y be Subset of cPR st P1[n, x, y];

            end;

          end;

          consider F be sequence of ( bool cPR) such that

           A6: (F . 0 ) = {( 0. PR)} & for n be Nat holds P1[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A2);

          defpred P2[ set, set] means ex n be Element of NAT , A,B be non empty Subset of cPR st A = (F . n) & B = (I \ (A -Ideal )) & n = $1 & (F . (n + 1)) = ((F . n) \/ {$2}) & $2 in ( minlen B);

          defpred P[ Nat] means (F . $1) is non empty finite Subset of I;

           A7:

          now

            let n be Nat;

            assume P[n];

            then

            reconsider Fn = (F . n) as non empty finite Subset of I;

            consider A,B be non empty Subset of cPR such that A = Fn and

             A8: B = (I \ (A -Ideal )) and

             A9: ex r be Element of cPR st r in ( minlen B) & (F . (n + 1)) = (Fn \/ {r}) by A6;

            consider r be Element of cPR such that

             A10: r in ( minlen B) and

             A11: (F . (n + 1)) = (Fn \/ {r}) by A9;

            r in I by A8, A10, XBOOLE_0:def 5;

            then {r} c= I by ZFMISC_1: 31;

            hence P[(n + 1)] by A11, XBOOLE_1: 8;

          end;

          (F . 0 ) c= I

          proof

            let x be object;

            assume x in (F . 0 );

            then x = ( 0. PR) by A6, TARSKI:def 1;

            hence thesis by IDEAL_1: 2;

          end;

          then

           A12: P[ 0 ] by A6;

          

           A13: for n be Nat holds P[n] from NAT_1:sch 2( A12, A7);

           A14:

          now

            let x be Element of NAT ;

            ex A,B be non empty Subset of cPR st A = (F . x) & B = (I \ (A -Ideal )) & ex r be Element of cPR st r in ( minlen B) & (F . (x + 1)) = ((F . x) \/ {r}) by A6, A13;

            hence ex y be Element of cPR st P2[x, y];

          end;

          consider f be sequence of cPR such that

           A15: for x be Element of NAT holds P2[x, (f . x)] from FUNCT_2:sch 3( A14);

          

           A16: for x be Nat holds P2[x, (f . x)]

          proof

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            hence thesis by A15;

          end;

          

           A17: for i,j be Element of NAT st i <= j holds (F . i) c= (F . j)

          proof

            let i,j be Element of NAT ;

            defpred P[ Nat] means (F . i) c= (F . (i + $1));

            assume i <= j;

            then

            consider m be Nat such that

             A18: j = (i + m) by NAT_1: 10;

            

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

            proof

              let m be Nat;

              ex A,B be non empty Subset of cPR st A = (F . (i + m)) & B = (I \ (A -Ideal )) & ex r be Element of cPR st r in ( minlen B) & (F . ((i + m) + 1)) = ((F . (i + m)) \/ {r}) by A6, A13;

              then

               A20: (F . (i + m)) c= (F . ((i + m) + 1)) by XBOOLE_1: 7;

              assume (F . i) c= (F . (i + m));

              hence thesis by A20, XBOOLE_1: 1;

            end;

            

             A21: P[ 0 ];

            

             A22: for m be Nat holds P[m] from NAT_1:sch 2( A21, A19);

            thus thesis by A18, A22;

          end;

          

           A23: for i be Element of NAT holds (f . i) <> ( 0. PR)

          proof

            let i be Element of NAT ;

            consider n be Element of NAT , A,B be non empty Subset of cPR such that

             A24: A = (F . n) and

             A25: B = (I \ (A -Ideal )) and n = i and (F . (n + 1)) = ((F . n) \/ {(f . i)}) and

             A26: (f . i) in ( minlen B) by A16;

            (F . n) c= (A -Ideal ) by A24, IDEAL_1:def 14;

            then

             A27: not (f . i) in (F . n) by A25, A26, XBOOLE_0:def 5;

            (F . 0 ) c= (F . n) & ( 0. PR) in (F . 0 ) by A6, A17, TARSKI:def 1;

            hence thesis by A27;

          end;

           A28:

          now

            let i be Element of NAT , fi be Polynomial of R;

            assume fi = (f . i);

            then fi <> ( 0. PR) by A23;

            then fi <> ( 0_. R) by POLYNOM3:def 10;

            then ( len fi) <> 0 by POLYNOM4: 5;

            then ( len fi) >= ( 0 + 1) by NAT_1: 13;

            hence (( len fi) - 1) >= 0 by XREAL_1: 19;

          end;

          defpred P3[ set, set] means ex n be Element of NAT , A be Polynomial of R st n = $1 & A = (f . n) & $2 = (A . (( len A) -' 1));

           A29:

          now

            let x be Element of NAT ;

            reconsider fx = (f . x) as Polynomial of R by POLYNOM3:def 10;

            (fx . (( len fx) -' 1)) is Element of cR;

            hence ex y be Element of cR st P3[x, y];

          end;

          consider a be sequence of cR such that

           A30: for x be Element of NAT holds P3[x, (a . x)] from FUNCT_2:sch 3( A29);

          reconsider a as sequence of R;

          for B be non empty Subset of cR holds ex C be non empty finite Subset of cR st C c= B & (C -Ideal ) = (B -Ideal ) by IDEAL_1: 96;

          then

          consider m be Element of NAT such that

           A31: (a . (m + 1)) in (( rng (a | (m + 1))) -Ideal ) by IDEAL_1: 97;

          reconsider fm1 = (f . (m + 1)) as Polynomial of R by POLYNOM3:def 10;

          defpred P4[ object, object] means (ex u,v,w be Element of cR st $1 = ((u * v) * w) & v in ( rng (a | ( Segm (m + 1))))) implies ex x,y,z be Element of cPR, p be Polynomial of R st $2 = p & p = ((x * y) * z) & $1 = (p . (( len fm1) -' 1)) & ( len p) <= ( len fm1) & y in (F . (m + 1));

          

           A32: ex n be Element of NAT , A,B be non empty Subset of cPR st A = (F . n) & B = (I \ (A -Ideal )) & n = (m + 1) & (F . (n + 1)) = ((F . n) \/ {(f . (m + 1))}) & (f . (m + 1)) in ( minlen B) by A16;

          

           A33: for i,j be Element of NAT , fi,fj be Polynomial of R st i <= j & fi = (f . i) & fj = (f . j) holds ( len fi) <= ( len fj)

          proof

            let i,j be Element of NAT , fi,fj be Polynomial of R;

            assume that

             A34: i <= j and

             A35: fi = (f . i) and

             A36: fj = (f . j);

            consider k be Nat such that

             A37: j = (i + k) by A34, NAT_1: 10;

            defpred P[ Nat] means for fk be Polynomial of R st fk = (f . (i + $1)) holds ( len fi) <= ( len fk);

             A38:

            now

              let k be Nat;

              assume

               A39: P[k];

              now

                reconsider fk = (f . (i + k)) as Polynomial of R by POLYNOM3:def 10;

                let fk1 be Polynomial of R;

                

                 A40: ( len fi) <= ( len fk) by A39;

                consider n be Element of NAT , A,B be non empty Subset of cPR such that

                 A41: A = (F . n) and

                 A42: B = (I \ (A -Ideal )) and

                 A43: n = (i + k) and (F . (n + 1)) = ((F . n) \/ {(f . (i + k))}) and

                 A44: (f . (i + k)) in ( minlen B) by A16;

                consider n9 be Element of NAT , A9,B9 be non empty Subset of cPR such that

                 A45: A9 = (F . n9) and

                 A46: B9 = (I \ (A9 -Ideal )) and

                 A47: n9 = (i + (k + 1)) and (F . (n9 + 1)) = ((F . n9) \/ {(f . (i + (k + 1)))}) and

                 A48: (f . (i + (k + 1))) in ( minlen B9) by A16;

                

                 A49: (f . (i + (k + 1))) in I by A46, A48, XBOOLE_0:def 5;

                (i + (k + 1)) = ((i + k) + 1);

                then (i + k) < (i + (k + 1)) by NAT_1: 13;

                then (A -Ideal ) c= (A9 -Ideal ) by A17, A41, A43, A45, A47, IDEAL_1: 57;

                then not (f . (i + (k + 1))) in (A -Ideal ) by A46, A48, XBOOLE_0:def 5;

                then

                 A50: (f . (i + (k + 1))) in B by A42, A49, XBOOLE_0:def 5;

                assume fk1 = (f . (i + (k + 1)));

                then ( len fk) <= ( len fk1) by A44, A50, Th17;

                hence ( len fi) <= ( len fk1) by A40, XXREAL_0: 2;

              end;

              hence P[(k + 1)];

            end;

            

             A51: P[ 0 ] by A35;

            

             A52: for k be Nat holds P[k] from NAT_1:sch 2( A51, A38);

            thus thesis by A36, A37, A52;

          end;

          

           A53: for e be object st e in cR holds ex d be object st d in cPR & P4[e, d]

          proof

            let e be object;

            assume e in cR;

            per cases ;

              suppose ex u,v,w be Element of cR st e = ((u * v) * w) & v in ( rng (a | ( Segm (m + 1))));

              then

              consider u,b9,w be Element of cR such that

               A54: e = ((u * b9) * w) and

               A55: b9 in ( rng (a | ( Segm (m + 1))));

              consider n be object such that

               A56: n in ( dom (a | ( Segm (m + 1)))) and

               A57: b9 = ((a | ( Segm (m + 1))) . n) by A55, FUNCT_1:def 3;

              set c9 = w;

              set a9 = u;

              set z9 = ( monomial (c9, 0 ));

              

               A58: (( len fm1) -' 1) = ((( len fm1) -' 1) + 0 );

              reconsider n as Element of NAT by A56;

              set y = (f . n);

              reconsider y9 = y as Polynomial of R by POLYNOM3:def 10;

              set x9 = ( monomial (a9,(( len fm1) -' ( len y9))));

              ( dom (a | ( Segm (m + 1)))) = (( dom a) /\ ( Segm (m + 1))) by RELAT_1: 61

              .= ( NAT /\ ( Segm (m + 1))) by FUNCT_2:def 1

              .= ( Segm (m + 1)) by XBOOLE_1: 28;

              then

               A59: n < (m + 1) by A56, NAT_1: 44;

              then ( len y9) <= ( len fm1) by A33;

              then (( len y9) - ( len y9)) <= (( len fm1) - ( len y9)) by XREAL_1: 9;

              then

               A60: (( len fm1) -' ( len y9)) = (( len fm1) - ( len y9)) by XREAL_0:def 2;

              then ( len x9) <= ((( len fm1) - ( len y9)) + 1) by Th18;

              then

               A61: (( len x9) + (( len y9) - 1)) <= ((( len fm1) - (( len y9) - 1)) + (( len y9) - 1)) by XREAL_1: 6;

              

               A62: ( len (x9 *' y9)) <= ((( len x9) + ( len y9)) -' 1) by Th21;

              

               A63: (( len y9) - 1) >= 0 by A28;

              then ( 0 + 0 ) <= ((( len y9) - 1) + ( len x9));

              then ( len (x9 *' y9)) <= ((( len x9) + ( len y9)) - 1) by A62, XREAL_0:def 2;

              then

               A64: ( len (x9 *' y9)) <= ( len fm1) by A61, XXREAL_0: 2;

              (( len fm1) - 1) >= 0 by A28;

              

              then

               A65: (( len fm1) -' 1) = ((( len fm1) - ( len y9)) + (( len y9) - 1)) by XREAL_0:def 2

              .= ((( len y9) -' 1) + (( len fm1) -' ( len y9))) by A60, A63, XREAL_0:def 2;

              reconsider x = x9, z = z9 as Element of cPR by POLYNOM3:def 10;

              set p = ((x * y) * z);

              

               A66: (x * y) = (x9 *' y9) by POLYNOM3:def 10;

              then

               A67: p = ((x9 *' y9) *' z9) by POLYNOM3:def 10;

              reconsider p as Polynomial of R by POLYNOM3:def 10;

              

               A68: ex n9 be Element of NAT , A be Polynomial of R st n9 = n & A = (f . n9) & (a . n) = (A . (( len A) -' 1)) by A30;

              b9 = (a . n) by A56, A57, FUNCT_1: 47;

              then ((x9 *' y9) . (( len fm1) -' 1)) = (a9 * b9) by A68, A65, Th19;

              then

               A69: ((a9 * b9) * c9) = (p . (( len fm1) -' 1)) by A67, A58, Th20;

              ex n9 be Element of NAT , A,B be non empty Subset of cPR st A = (F . n9) & B = (I \ (A -Ideal )) & n9 = n & (F . (n9 + 1)) = ((F . n9) \/ {(f . n)}) & (f . n) in ( minlen B) by A16;

              then {y} c= (F . (n + 1)) by XBOOLE_1: 7;

              then

               A70: y in (F . (n + 1)) by ZFMISC_1: 31;

              ( len z9) <= ( 0 + 1) by Th18;

              then (( len (x9 *' y9)) + ( len z9)) <= (( len fm1) + 1) by A64, XREAL_1: 7;

              then

               A71: ((( len (x9 *' y9)) + ( len z9)) -' 1) <= ((( len fm1) + 1) -' 1) by NAT_D: 42;

              ( len ((x9 *' y9) *' z9)) <= ((( len (x9 *' y9)) + ( len z9)) -' 1) by Th21;

              then ( len ((x9 *' y9) *' z9)) <= ((( len fm1) + 1) -' 1) by A71, XXREAL_0: 2;

              then ( len ((x9 *' y9) *' z9)) <= ((( len fm1) + 1) - 1) by XREAL_0:def 2;

              then

               A72: ( len p) <= (( len fm1) + 0 ) by A66, POLYNOM3:def 10;

              (n + 1) <= (m + 1) by A59, NAT_1: 13;

              then (F . (n + 1)) c= (F . (m + 1)) by A17;

              hence thesis by A54, A69, A72, A70;

            end;

              suppose not ex u,v,w be Element of cR st e = ((u * v) * w) & v in ( rng (a | ( Segm (m + 1))));

              hence thesis;

            end;

          end;

          consider LCT be Function of cR, cPR such that

           A73: for e be object st e in cR holds P4[e, (LCT . e)] from FUNCT_2:sch 1( A53);

          reconsider FM1 = (F . (m + 1)) as non empty Subset of cPR by A13;

          set raSm1 = ( rng (a | ( Segm (m + 1))));

          consider lc be LinearCombination of ( rng (a | ( Segm (m + 1)))) such that

           A74: (a . (m + 1)) = ( Sum lc) by A31, IDEAL_1: 60;

          

           A75: for lc be LinearCombination of raSm1 holds ex LC be LinearCombination of FM1 st LC = (LCT * lc) & ( len lc) = ( len LC)

          proof

            let lc be LinearCombination of raSm1;

            set LC = (LCT * lc);

            ( dom LCT) = cR by FUNCT_2:def 1;

            then ( rng lc) c= ( dom LCT);

            then

             A76: ( dom lc) = ( dom (LCT * lc)) by RELAT_1: 27;

            then

             A77: ( len lc) = ( len LC) by FINSEQ_3: 29;

            LC is LinearCombination of FM1

            proof

              let i be set such that

               A78: i in ( dom LC);

              consider u,v be Element of R, a be Element of raSm1 such that

               A79: (lc /. i) = ((u * a) * v) by A76, A78, IDEAL_1:def 8;

              

               A80: (lc /. i) = (lc . i) by A76, A78, PARTFUN1:def 6;

              consider x,y,z be Element of cPR, p be Polynomial of R such that

               A81: (LCT . (lc /. i)) = p & p = ((x * y) * z) and ((u * a) * v) = (p . (( len fm1) -' 1)) and ( len p) <= ( len fm1) and

               A82: y in (F . (m + 1)) by A73, A79;

              reconsider y as Element of FM1 by A82;

              reconsider x, z as Element of PR;

              (LC /. i) = ((LCT * lc) . i) by A78, PARTFUN1:def 6

              .= ((x * y) * z) by A76, A78, A80, A81, FUNCT_1: 13;

              hence ex x,z be Element of PR, y be Element of FM1 st (LC /. i) = ((x * y) * z);

            end;

            then

            reconsider LC as LinearCombination of FM1;

            LC = LC;

            hence thesis by A77;

          end;

          for lc be LinearCombination of raSm1 holds ex LC be LinearCombination of FM1, sLC be Polynomial of R st LC = (LCT * lc) & sLC = ( Sum LC) & (sLC . (( len fm1) -' 1)) = ( Sum lc) & ( len sLC) <= ( len fm1)

          proof

            let lc be LinearCombination of raSm1;

            defpred P5[ Nat] means for lc be LinearCombination of raSm1 st ( len lc) <= $1 holds ex LC be LinearCombination of FM1, sLC be Polynomial of R st LC = (LCT * lc) & sLC = ( Sum LC) & (sLC . (( len fm1) -' 1)) = ( Sum lc) & ( len sLC) <= ( len fm1);

            

             A83: ex n be Element of NAT st n = ( len lc);

            

             A84: for k be Nat st P5[k] holds P5[(k + 1)]

            proof

              let k be Nat;

              assume

               A85: P5[k];

              thus P5[(k + 1)]

              proof

                let lc be LinearCombination of raSm1;

                assume

                 A86: ( len lc) <= (k + 1);

                per cases ;

                  suppose ( len lc) <= k;

                  hence thesis by A85;

                end;

                  suppose

                   A87: ( len lc) > k;

                  then ( len lc) >= (k + 1) by NAT_1: 13;

                  then

                   A88: ( len lc) = (k + 1) by A86, XXREAL_0: 1;

                  thus thesis

                  proof

                    per cases ;

                      suppose

                       A89: k = 0 ;

                      then ( dom lc) = {1} by A88, FINSEQ_1: 2, FINSEQ_1:def 3;

                      then

                       A90: 1 in ( dom lc) by TARSKI:def 1;

                      then

                      consider u,w be Element of R, v be Element of raSm1 such that

                       A91: (lc /. 1) = ((u * v) * w) by IDEAL_1:def 8;

                      

                       A92: (lc . 1) = (lc /. 1) by A90, PARTFUN1:def 6;

                      then

                      consider x,y,z be Element of cPR, p be Polynomial of R such that

                       A93: (LCT . (lc . 1)) = p and p = ((x * y) * z) and

                       A94: ((u * v) * w) = (p . (( len fm1) -' 1)) and

                       A95: ( len p) <= ( len fm1) and y in (F . (m + 1)) by A73, A91;

                      

                       A96: lc = <*(lc . 1)*> by A88, A89, FINSEQ_1: 40;

                      then

                       A97: ( Sum lc) = (p . (( len fm1) -' 1)) by A91, A92, A94, RLVECT_1: 44;

                      consider LC be LinearCombination of FM1 such that

                       A98: LC = (LCT * lc) and ( len LC) = ( len lc) by A75;

                      LC = <*(LCT . ((u * v) * w))*> by A96, A91, A92, A98, FINSEQ_2: 35;

                      then ( Sum LC) = p by A91, A92, A93, RLVECT_1: 44;

                      hence thesis by A95, A98, A97;

                    end;

                      suppose

                       A99: k > 0 ;

                      consider LC be LinearCombination of FM1 such that

                       A100: LC = (LCT * lc) and ( len LC) = ( len lc) by A75;

                      lc is non empty by A87;

                      then

                      consider p be LinearCombination of raSm1, e be Element of cR such that

                       A101: lc = (p ^ <*e*>) and

                       A102: <*e*> is LinearCombination of raSm1 by IDEAL_1: 32;

                      ( len <*e*>) = ( 0 + 1) by FINSEQ_1: 39;

                      then ( len <*e*>) <= k by A99, NAT_1: 13;

                      then

                      consider LCe be LinearCombination of FM1, sLCe be Polynomial of R such that

                       A103: LCe = (LCT * <*e*>) and

                       A104: sLCe = ( Sum LCe) and

                       A105: (sLCe . (( len fm1) -' 1)) = ( Sum <*e*>) and

                       A106: ( len sLCe) <= ( len fm1) by A85, A102;

                      ( len lc) = (( len p) + ( len <*e*>)) by A101, FINSEQ_1: 22

                      .= (( len p) + 1) by FINSEQ_1: 39;

                      then

                      consider LCp be LinearCombination of FM1, sLCp be Polynomial of R such that

                       A107: LCp = (LCT * p) and

                       A108: sLCp = ( Sum LCp) and

                       A109: (sLCp . (( len fm1) -' 1)) = ( Sum p) and

                       A110: ( len sLCp) <= ( len fm1) by A85, A88;

                      set sLC = (sLCp + sLCe);

                      

                       A111: ( Sum lc) = (( Sum p) + e) by A101, FVSUM_1: 71

                      .= ((sLCp . (( len fm1) -' 1)) + (sLCe . (( len fm1) -' 1))) by A109, A105, RLVECT_1: 44

                      .= (sLC . (( len fm1) -' 1)) by NORMSP_1:def 2;

                       A112:

                      now

                        per cases ;

                          suppose ( len sLCp) < ( len sLCe);

                          then ( len sLC) <= ( len sLCe) by POLYNOM4: 6;

                          hence ( len sLC) <= ( len fm1) by A106, XXREAL_0: 2;

                        end;

                          suppose ( len sLCp) >= ( len sLCe);

                          then ( len sLC) <= ( len sLCp) by POLYNOM4: 6;

                          hence ( len sLC) <= ( len fm1) by A110, XXREAL_0: 2;

                        end;

                      end;

                      ( dom LCT) = cR by FUNCT_2:def 1;

                      then (( rng p) \/ ( rng <*e*>)) c= ( dom LCT);

                      then ex LCTp,LCTe be FinSequence st LCTp = (LCT * p) & LCTe = (LCT * <*e*>) & (LCT * (p ^ <*e*>)) = (LCTp ^ LCTe) by Th1;

                      

                      then ( Sum LC) = (( Sum LCp) + ( Sum LCe)) by A101, A107, A103, A100, RLVECT_1: 41

                      .= sLC by A108, A104, POLYNOM3:def 10;

                      hence thesis by A100, A111, A112;

                    end;

                  end;

                end;

              end;

            end;

            

             A113: P5[ 0 ]

            proof

              let lc be LinearCombination of raSm1;

              assume

               A114: ( len lc) <= 0 ;

              then

               A115: lc = ( <*> cR);

              consider LC be LinearCombination of FM1 such that

               A116: LC = (LCT * lc) and

               A117: ( len lc) = ( len LC) by A75;

              take LC, p = ( 0_. R);

              thus LC = (LCT * lc) by A116;

              LC = ( <*> cPR) by A114, A117;

              

              then ( Sum LC) = ( 0. PR) by RLVECT_1: 43

              .= p by POLYNOM3:def 10;

              hence p = ( Sum LC);

              

              thus (p . (( len fm1) -' 1)) = ( 0. R)

              .= ( Sum lc) by A115, RLVECT_1: 43;

              thus thesis by POLYNOM4: 3;

            end;

            for k be Nat holds P5[k] from NAT_1:sch 2( A113, A84);

            hence thesis by A83;

          end;

          then

          consider LC be LinearCombination of FM1, sLC be Polynomial of R such that LC = (LCT * lc) and

           A118: sLC = ( Sum LC) and

           A119: (sLC . (( len fm1) -' 1)) = ( Sum lc) and

           A120: ( len sLC) <= ( len fm1);

          

           A121: sLC in (FM1 -Ideal ) by A118, IDEAL_1: 60;

          set f9 = (fm1 - sLC);

           A122:

          now

            ex n be Element of NAT , A be Polynomial of R st n = (m + 1) & A = (f . n) & (a . (m + 1)) = (A . (( len A) -' 1)) by A30;

            

            then

             A123: (f9 . (( len fm1) -' 1)) = ((fm1 . (( len fm1) -' 1)) - (fm1 . (( len fm1) -' 1))) by A74, A119, POLYNOM3: 27

            .= ( 0. R) by RLVECT_1: 15;

            (( len fm1) - 1) >= 0 by A28;

            

            then

             A124: ((( len fm1) -' 1) + 1) = ((( len fm1) - 1) + 1) by XREAL_0:def 2

            .= ( len fm1);

            assume ( len f9) = ( len fm1);

            hence contradiction by A124, A123, ALGSEQ_1: 10;

          end;

          

           A125: (f9 + sLC) = (fm1 + (sLC + ( - sLC))) by POLYNOM3: 26

          .= (fm1 + (sLC - sLC))

          .= (fm1 + ( 0_. R)) by POLYNOM3: 29

          .= fm1 by POLYNOM3: 28;

           A126:

          now

            reconsider sLC as Element of cPR by POLYNOM3:def 10;

            assume

             A127: f9 in (FM1 -Ideal );

            reconsider f9 as Element of cPR by POLYNOM3:def 10;

            (f . (m + 1)) = (f9 + sLC) by A125, POLYNOM3:def 10;

            then fm1 in (FM1 -Ideal ) by A121, A127, IDEAL_1:def 1;

            hence contradiction by A32, XBOOLE_0:def 5;

          end;

          ( len ( - sLC)) <= ( len fm1) by A120, POLYNOM4: 8;

          then ( len f9) <= ( len fm1) by POLYNOM4: 6;

          then

           A128: ( len f9) < ( len fm1) by A122, XXREAL_0: 1;

          f9 in I

          proof

            reconsider f9 as Element of cPR by POLYNOM3:def 10;

            reconsider sLC as Element of cPR by POLYNOM3:def 10;

            FM1 is Subset of I by A13;

            then (FM1 -Ideal ) c= (I -Ideal ) by IDEAL_1: 57;

            then

             A129: (FM1 -Ideal ) c= I by IDEAL_1: 44;

            (f . (m + 1)) in I & f9 = ((f . (m + 1)) - sLC) by A32, Th16, XBOOLE_0:def 5;

            hence thesis by A121, A129, IDEAL_1: 15;

          end;

          then f9 in (I \ (FM1 -Ideal )) by A126, XBOOLE_0:def 5;

          hence contradiction by A128, A32, Th17;

        end;

        hence thesis;

      end;

    end

    theorem :: HILBASIS:32

    

     Th32: for R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial doubleLoopStr st R is Noetherian holds for n be Nat holds ( Polynom-Ring (n,R)) is Noetherian

    proof

      let R be Abelian add-associative right_zeroed right_complementable associative distributive well-unital commutative non trivial doubleLoopStr;

      assume

       A1: R is Noetherian;

      defpred P[ Nat] means ( Polynom-Ring ($1,R)) is Noetherian;

       A2:

      now

        let k be Nat such that

         A3: P[k];

        ex P be Function of ( Polynom-Ring ( Polynom-Ring (k,R))), ( Polynom-Ring ((k + 1),R)) st P is RingIsomorphism by Th31;

        hence P[(k + 1)] by A3, Th27;

      end;

      ex P be Function of R, ( Polynom-Ring ( 0 ,R)) st P is RingIsomorphism by Th28;

      then

       A4: P[ 0 ] by A1, Th27;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

    end;

    theorem :: HILBASIS:33

    

     Th33: for F be Field holds F is Noetherian

    proof

      let F be Field;

      let I be Ideal of F;

      per cases by IDEAL_1: 22;

        suppose

         A1: I = {( 0. F)};

        reconsider s0F = {( 0. F)} as finite non empty Subset of F;

         {( 0. F)} = (s0F -Ideal ) by IDEAL_1: 47;

        hence thesis by A1;

      end;

        suppose

         A2: I = the carrier of F;

        reconsider s1F = {( 1_ F)} as finite non empty Subset of F;

        the carrier of F = (s1F -Ideal ) by IDEAL_1: 51;

        hence thesis by A2;

      end;

    end;

    theorem :: HILBASIS:34

    for F be Field, n be Element of NAT holds ( Polynom-Ring (n,F)) is Noetherian

    proof

      let F be Field, n be Element of NAT ;

      F is Noetherian by Th33;

      hence thesis by Th32;

    end;

    theorem :: HILBASIS:35

    for R be Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, X be infinite Ordinal holds ( Polynom-Ring (X,R)) is non Noetherian

    proof

      deffunc F( set) = $1;

      let R be Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, X be infinite Ordinal such that

       A1: ( Polynom-Ring (X,R)) is Noetherian;

      reconsider f0 = (X --> ( 0. R)) as Function of X, the carrier of R;

      deffunc G( Element of X) = ( 1_1 ($1,R));

      set tcR = the carrier of R;

      

       A2: for d1,d2 be Element of X st G(d1) = G(d2) holds d1 = d2 by Th14;

      tcR c= tcR;

      then

      reconsider cR = the carrier of R as non empty Subset of tcR;

      set S = { ( 1_1 (n,R)) where n be Element of X : n in NAT };

      set tcPR = the carrier of ( Polynom-Ring (X,R));

      

       A3: NAT c= X by CARD_3: 85;

      reconsider 0X = 0 as Element of X by A3;

      

       A4: S c= tcPR

      proof

        let x be object;

        assume x in S;

        then ex n be Element of X st x = ( 1_1 (n,R)) & n in NAT ;

        hence thesis by POLYNOM1:def 11;

      end;

      ( 1_1 (0X,R)) in S;

      then

      reconsider S as non empty Subset of tcPR by A4;

      consider C be non empty finite Subset of tcPR such that

       A5: C c= S and

       A6: (C -Ideal ) = (S -Ideal ) by A1, IDEAL_1: 96;

      set CN = { F(n) where n be Element of X : G(n) in C };

      

       A7: C is finite;

      

       A8: CN is finite from FUNCT_7:sch 2( A7, A2);

      

       A9: CN c= NAT

      proof

        let x be object;

        assume x in CN;

        then

        consider n be Element of X such that

         A10: x = n and

         A11: ( 1_1 (n,R)) in C;

        ( 1_1 (n,R)) in S by A5, A11;

        then ex m be Element of X st ( 1_1 (n,R)) = ( 1_1 (m,R)) & m in NAT ;

        hence thesis by A10, Th14;

      end;

      set c = the Element of C;

      c in S by A5;

      then

      consider cn be Element of X such that

       A12: c = ( 1_1 (cn,R)) and

       A13: cn in NAT ;

      reconsider cn as Element of NAT by A13;

      cn in CN by A12;

      then

      reconsider CN as non empty finite Subset of NAT by A8, A9;

      reconsider mm = ( max CN) as Element of NAT by ORDINAL1:def 12;

      reconsider m1 = (mm + 1) as Element of NAT ;

      reconsider m2 = m1 as Element of X by A3;

      ( 1_1 (m2,R)) in S & S c= (S -Ideal ) by IDEAL_1:def 14;

      then

      consider lc be LinearCombination of C such that

       A14: ( 1_1 (m2,R)) = ( Sum lc) by A6, IDEAL_1: 60;

      reconsider ev = (f0 +* (m2,( 1_ R))) as Function of X, R;

      consider E be FinSequence of [:tcPR, tcPR, tcPR:] such that

       A15: E represents lc by IDEAL_1: 35;

      set P = ( Polynom-Evaluation (X,R,ev));

      deffunc F( Nat) = (((P . ((E /. $1) `1_3 )) * (P . ((E /. $1) `2_3 ))) * (P . ((E /. $1) `3_3 )));

      consider LC be FinSequence of the carrier of R such that

       A16: ( len LC) = ( len lc) and

       A17: for k be Nat st k in ( dom LC) holds (LC . k) = F(k) from FINSEQ_2:sch 1;

      now

        let i be set;

        assume

         A18: i in ( dom LC);

        then

        reconsider k = i as Element of NAT ;

        reconsider a = (P . ((E /. k) `2_3 )) as Element of cR;

        reconsider u = (P . ((E /. k) `1_3 )), v = (P . ((E /. k) `3_3 )) as Element of R;

        take u, v, a;

        

        thus (LC /. i) = (LC . k) by A18, PARTFUN1:def 6

        .= ((u * a) * v) by A17, A18;

      end;

      then

      reconsider LC as LinearCombination of cR by IDEAL_1:def 8;

       A19:

      now

        let i be Element of NAT ;

         A20:

        now

          assume m2 in CN;

          then (( max CN) + 1) <= ( max CN) by XXREAL_2:def 8;

          hence contradiction by XREAL_1: 29;

        end;

        assume

         A21: i in ( dom LC);

        then i in ( dom lc) by A16, FINSEQ_3: 29;

        then

        reconsider y = ((E /. i) `2_3 ) as Element of C by A15;

        y in S by A5;

        then

        consider n be Element of X such that

         A22: y = ( 1_1 (n,R)) and n in NAT ;

        n in CN by A22;

        

        then

         A23: (ev . n) = ((X --> ( 0. R)) . n) by A20, FUNCT_7: 32

        .= ( 0. R);

        

         A24: ( Support ( 1_1 (n,R))) = {( UnitBag n)} by Th13;

        

         A25: (P . ( 1_1 (n,R))) = ( eval (( 1_1 (n,R)),ev)) by POLYNOM2:def 5

        .= ((( 1_1 (n,R)) . ( UnitBag n)) * ( eval (( UnitBag n),ev))) by A24, POLYNOM2: 19

        .= (( 1_ R) * ( eval (( UnitBag n),ev))) by Th12

        .= (( 1_ R) * (ev . n)) by Th11

        .= ( 0. R) by A23;

        

        thus (LC . i) = (((P . ((E /. i) `1_3 )) * (P . ((E /. i) `2_3 ))) * (P . ((E /. i) `3_3 ))) by A17, A21

        .= (( 0. R) * (P . ((E /. i) `3_3 ))) by A22, A25

        .= ( 0. R);

      end;

      ( dom (X --> ( 0. R))) = X;

      then

       A26: (ev . m2) = ( 1_ R) by FUNCT_7: 31;

      

       A27: ( Support ( 1_1 (m2,R))) = {( UnitBag m2)} by Th13;

      

       A28: (( Polynom-Evaluation (X,R,ev)) . ( 1_1 (m2,R))) = ( eval (( 1_1 (m2,R)),ev)) by POLYNOM2:def 5

      .= ((( 1_1 (m2,R)) . ( UnitBag m2)) * ( eval (( UnitBag m2),ev))) by A27, POLYNOM2: 19

      .= (( 1_ R) * ( eval (( UnitBag m2),ev))) by Th12

      .= (( 1_ R) * (ev . m2)) by Th11

      .= ( 1_ R) by A26;

      for k be set st k in ( dom LC) holds (LC . k) = (((P . ((E /. k) `1_3 )) * (P . ((E /. k) `2_3 ))) * (P . ((E /. k) `3_3 ))) by A17;

      

      then (P . ( Sum lc)) = ( Sum LC) by A15, A16, Th24

      .= ( 0. R) by A19, POLYNOM3: 1;

      hence contradiction by A14, A28;

    end;