polyred.miz



    begin

    registration

      let n be Ordinal, R be non trivial ZeroStr;

      cluster non-zero for Monomial of n, R;

      existence

      proof

        set a = the Element of ( NonZero R);

        reconsider a as Element of R;

        take q = (a | (n,R));

        

         A1: a <> ( 0. R) & ( 0_ (n,R)) = (( 0. R) | (n,R)) by POLYNOM7: 19, ZFMISC_1: 56;

        assume q = ( 0_ (n,R));

        hence contradiction by A1, POLYNOM7: 21;

      end;

    end

    registration

      cluster non trivial for Field;

      existence

      proof

        set F = the Field;

        take F;

        thus thesis;

      end;

    end

    

     Lm1: for X be set, S be Subset of X, R be Order of X st R is being_linear-order holds R linearly_orders S

    proof

      let X be set, S be Subset of X, R be Order of X;

      S c= X;

      then

       A1: S c= ( field R) by ORDERS_1: 15;

      assume R is being_linear-order;

      hence thesis by A1, ORDERS_1: 37, ORDERS_1: 38;

    end;

    

     Lm2: for n be Ordinal, b1,b2,b3 be bag of n holds b1 <=' b2 implies (b1 + b3) <=' (b2 + b3)

    proof

      let n be Ordinal, b1,b2,b3 be bag of n;

      assume

       A1: b1 <=' b2;

      per cases ;

        suppose b1 = b2;

        hence thesis;

      end;

        suppose b1 <> b2;

        then b1 < b2 by A1, PRE_POLY:def 10;

        then

        consider k be Ordinal such that

         A2: (b1 . k) < (b2 . k) and

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

         A4:

        now

          let l be Ordinal;

          assume

           A5: l in k;

          

          thus ((b1 + b3) . l) = ((b1 . l) + (b3 . l)) by PRE_POLY:def 5

          .= ((b2 . l) + (b3 . l)) by A3, A5

          .= ((b2 + b3) . l) by PRE_POLY:def 5;

        end;

        ((b1 + b3) . k) = ((b1 . k) + (b3 . k)) & ((b2 + b3) . k) = ((b2 . k) + (b3 . k)) by PRE_POLY:def 5;

        then ((b1 + b3) . k) < ((b2 + b3) . k) by A2, XREAL_1: 8;

        then (b1 + b3) < (b2 + b3) by A4, PRE_POLY:def 9;

        hence thesis by PRE_POLY:def 10;

      end;

    end;

    

     Lm3: for n be Ordinal, b1,b2 be bag of n holds b1 <=' b2 & b2 <=' b1 implies b1 = b2

    proof

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

      assume that

       A1: b1 <=' b2 and

       A2: b2 <=' b1;

      now

        assume

         A3: b1 <> b2;

        then b1 < b2 by A1, PRE_POLY:def 10;

        hence contradiction by A2, A3, PRE_POLY:def 10;

      end;

      hence thesis;

    end;

    

     Lm4: for n be Ordinal, b1,b2 be bag of n holds not b1 < b2 iff b2 <=' b1

    proof

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

       A1:

      now

        assume

         A2: not b1 < b2;

        now

          per cases ;

            case b1 = b2;

            hence b2 <=' b1;

          end;

            case b1 <> b2;

            then not b1 <=' b2 by A2, PRE_POLY:def 10;

            hence b2 <=' b1 by PRE_POLY: 45;

          end;

        end;

        hence b2 <=' b1;

      end;

      now

        assume

         A3: b2 <=' b1;

        now

          per cases ;

            case b2 <> b1;

            hence not b1 < b2 by A3, PRE_POLY:def 10;

          end;

            case b1 = b2;

            hence not (ex k be Ordinal st (b1 . k) < (b2 . k) & for l be Ordinal st l in k holds (b1 . l) = (b2 . l));

          end;

        end;

        hence not b1 < b2;

      end;

      hence thesis by A1;

    end;

    

     Lm5: for n be Ordinal, L be non trivial ZeroStr, p be non-zero finite-Support Series of n, L holds ex b be bag of n st (p . b) <> ( 0. L) & for b9 be bag of n st b < b9 holds (p . b9) = ( 0. L)

    proof

      let n be Ordinal, L be non trivial ZeroStr, p be non-zero finite-Support Series of n, L;

      defpred P[ Nat] means for B be finite Subset of ( Bags n) st ( card B) = $1 holds ex b be bag of n st b in B & for b9 be bag of n st b9 in B holds b9 <=' b;

      

       A1: for k be Nat st 1 <= k holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: 1 <= k;

        thus P[k] implies P[(k + 1)]

        proof

          assume

           A3: P[k];

          thus P[(k + 1)]

          proof

            let B be finite Subset of ( Bags n);

            assume

             A4: ( card B) = (k + 1);

            then

            reconsider B as non empty finite Subset of ( Bags n);

            set x = the Element of B;

            reconsider x as Element of ( Bags n);

            reconsider x as bag of n;

            set X = (B \ {x});

            now

              let u be object;

              assume u in {x};

              then u = x by TARSKI:def 1;

              hence u in B;

            end;

            then {x} c= B by TARSKI:def 3;

            

            then

             A5: B = ( {x} \/ B) by XBOOLE_1: 12

            .= ( {x} \/ X) by XBOOLE_1: 39;

            x in X iff x in B & not x in {x} by XBOOLE_0:def 5;

            then

             A6: (( card X) + 1) = (k + 1) by A4, A5, CARD_2: 41, TARSKI:def 1;

            then

            reconsider X as non empty set by A2, XCMPLX_1: 2;

            reconsider X as non empty finite Subset of ( Bags n);

            consider b be bag of n such that

             A7: b in X and

             A8: for b9 be bag of n st b9 in X holds b9 <=' b by A3, A6, XCMPLX_1: 2;

             A9:

            now

              per cases by PRE_POLY: 45;

                case

                 A10: x <=' b;

                now

                  let b9 be bag of n;

                  assume

                   A11: b9 in B;

                  now

                    per cases ;

                      case b9 in X;

                      hence b9 <=' b by A8;

                    end;

                      case not b9 in X;

                      then b9 in {x} by A5, A11, XBOOLE_0:def 3;

                      hence b9 <=' b by A10, TARSKI:def 1;

                    end;

                  end;

                  hence b9 <=' b;

                end;

                hence for b9 be bag of n st b9 in B holds b9 <=' b;

              end;

                case

                 A12: b <=' x;

                now

                  let b9 be bag of n;

                  assume

                   A13: b9 in B;

                  now

                    per cases ;

                      case b9 in X;

                      then b9 <=' b by A8;

                      hence b9 <=' x by A12, PRE_POLY: 42;

                    end;

                      case not b9 in X;

                      then b9 in {x} by A5, A13, XBOOLE_0:def 3;

                      hence b9 <=' x by TARSKI:def 1;

                    end;

                  end;

                  hence b9 <=' x;

                end;

                hence for b9 be bag of n st b9 in B holds b9 <=' x;

              end;

            end;

            b in B by A5, A7, XBOOLE_0:def 3;

            hence thesis by A9;

          end;

        end;

      end;

      reconsider sp = ( Support p) as finite set by POLYNOM1:def 5;

      

       A14: ( Support p) is finite Subset of ( Bags n) by POLYNOM1:def 5;

      ( card sp) is finite;

      then

      consider m be Nat such that

       A15: ( card ( Support p)) = ( card m) by CARD_1: 48;

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

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

      then m <> 0 by A15;

      then

       A16: 1 <= m by NAT_1: 14;

      

       A17: ( card ( Support p)) = m by A15;

      

       A18: P[1]

      proof

        let B be finite Subset of ( Bags n);

        assume ( card B) = 1;

        then ( card { {} }) = ( card B) by CARD_1: 30;

        then

        consider b be object such that

         A19: B = {b} by CARD_1: 29;

        

         A20: b in B by A19, TARSKI:def 1;

        then

        reconsider b as Element of ( Bags n);

        reconsider b as bag of n;

        for b9 be bag of n st b9 in B holds b9 <=' b by A19, TARSKI:def 1;

        hence thesis by A20;

      end;

      for k be Nat st 1 <= k holds P[k] from NAT_1:sch 8( A18, A1);

      then

      consider b be bag of n such that

       A21: b in ( Support p) and

       A22: for b9 be bag of n st b9 in ( Support p) holds b9 <=' b by A17, A16, A14;

       A23:

      now

        let b9 be bag of n;

        assume b < b9;

        then not b9 <=' b by Lm4;

        then

         A24: not b9 in ( Support p) by A22;

        b9 is Element of ( Bags n) by PRE_POLY:def 12;

        hence (p . b9) = ( 0. L) by A24, POLYNOM1:def 4;

      end;

      (p . b) <> ( 0. L) by A21, POLYNOM1:def 4;

      hence thesis by A23;

    end;

    

     Lm6: for L be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, f,g be FinSequence of the carrier of L, n be Nat st ( len f) = (n + 1) & g = (f | ( Seg n)) holds ( Sum f) = (( Sum g) + (f /. ( len f)))

    proof

      let L be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, f,g be FinSequence of the carrier of L, n be Nat;

      assume that

       A1: ( len f) = (n + 1) and

       A2: g = (f | ( Seg n));

      

       A3: n <= ( len f) by A1, NAT_1: 11;

      set q = <*(f /. ( len f))*>;

      set p = (g ^ q);

      

       A4: ( len q) = 1 by FINSEQ_1: 39;

      

       A5: ( dom f) = ( Seg (n + 1)) by A1, FINSEQ_1:def 3;

       A6:

      now

        let u be object;

        assume

         A7: u in ( dom f);

        then u in { k where k be Nat : 1 <= k & k <= (n + 1) } by A5, FINSEQ_1:def 1;

        then

        consider i be Nat such that

         A8: u = i and

         A9: 1 <= i and

         A10: i <= (n + 1);

        now

          per cases ;

            case

             A11: i = (n + 1);

            then (( len g) + 1) <= i & i <= (( len g) + ( len q)) by A2, A3, A4, FINSEQ_1: 17;

            

            hence (p . i) = (q . (i - ( len g))) by FINSEQ_1: 23

            .= (q . ((n + 1) - n)) by A2, A3, A11, FINSEQ_1: 17

            .= (q . 1) by XCMPLX_1: 26

            .= (f /. (n + 1)) by A1, FINSEQ_1: 40

            .= (f . i) by A7, A8, A11, PARTFUN1:def 6;

          end;

            case i <> (n + 1);

            then i < (n + 1) by A10, XXREAL_0: 1;

            then i <= n by NAT_1: 13;

            then i in { k where k be Nat : 1 <= k & k <= n } by A9;

            then i in ( Seg n) by FINSEQ_1:def 1;

            then

             A12: i in ( dom g) by A2, A3, FINSEQ_1: 17;

            then (p . i) = (g . i) by FINSEQ_1:def 7;

            hence (p . i) = (f . i) by A2, A12, FUNCT_1: 47;

          end;

        end;

        hence (f . u) = (p . u) by A8;

      end;

      ( len (g ^ q)) = (( len g) + ( len q)) by FINSEQ_1: 22

      .= (( len g) + 1) by FINSEQ_1: 40

      .= ( len f) by A1, A2, A3, FINSEQ_1: 17;

      

      then ( dom f) = ( Seg ( len (g ^ q))) by FINSEQ_1:def 3

      .= ( dom (g ^ q)) by FINSEQ_1:def 3;

      then f = (g ^ <*(f /. ( len f))*>) by A6, FUNCT_1: 2;

      

      hence ( Sum f) = (( Sum g) + ( Sum <*(f /. ( len f))*>)) by RLVECT_1: 41

      .= (( Sum g) + (f /. ( len f))) by RLVECT_1: 44;

    end;

    registration

      let n be Ordinal, L be add-associative right_complementable left_zeroed right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p,q be non-zero finite-Support Series of n, L;

      cluster (p *' q) -> non-zero;

      coherence

      proof

        consider b22 be bag of n such that

         A1: (q . b22) <> ( 0. L) and

         A2: for b9 be bag of n st b22 < b9 holds (q . b9) = ( 0. L) by Lm5;

        consider b11 be bag of n such that

         A3: (p . b11) <> ( 0. L) and

         A4: for b9 be bag of n st b11 < b9 holds (p . b9) = ( 0. L) by Lm5;

        set b = (b11 + b22);

        consider s be FinSequence of the carrier of L such that

         A5: ((p *' q) . b) = ( Sum s) and

         A6: ( len s) = ( len ( decomp b)) and

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

        

         A8: b is Element of ( Bags n) & ((p . b11) * (q . b22)) <> ( 0. L) by A3, A1, PRE_POLY:def 12, VECTSP_2:def 1;

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

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

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

        set sgm = ( SgmX (( BagOrder n),S));

        

         A11: ( BagOrder n) linearly_orders S by Lm1;

        b11 divides b by PRE_POLY: 50;

        then b11 in S by A10;

        then b11 in ( rng sgm) by A11, PRE_POLY:def 2;

        then

        consider i be object such that

         A12: i in ( dom sgm) and

         A13: (sgm . i) = b11 by FUNCT_1:def 3;

        

         A14: i in ( dom ( decomp b)) by A9, A12, PRE_POLY:def 17;

        (( divisors b) /. i) = b11 by A9, A12, A13, PARTFUN1:def 6;

        then

         A15: (( decomp b) /. i) = <*b11, (b -' b11)*> by A14, PRE_POLY:def 17;

        then

         A16: (( decomp b) /. i) = <*b11, b22*> by PRE_POLY: 48;

        

         A17: ( dom s) = ( Seg ( len ( decomp b))) by A6, FINSEQ_1:def 3

        .= ( dom ( decomp b)) by FINSEQ_1:def 3;

        then

         A18: i in ( dom s) by A9, A12, PRE_POLY:def 17;

        reconsider i as Element of NAT by A12;

        consider b1,b2 be bag of n such that

         A19: (( decomp b) /. i) = <*b1, b2*> and

         A20: (s /. i) = ((p . b1) * (q . b2)) by A7, A18;

        

         A21: b2 = ( <*b11, b22*> . 2) by A16, A19, FINSEQ_1: 44

        .= b22 by FINSEQ_1: 44;

         A22:

        now

          let k be Element of NAT ;

          assume that

           A23: k in ( dom s) and

           A24: k <> i;

          consider b1,b2 be bag of n such that

           A25: (( decomp b) /. k) = <*b1, b2*> and

           A26: (s /. k) = ((p . b1) * (q . b2)) by A7, A23;

          consider b19,b29 be bag of n such that

           A27: (( decomp b) /. k) = <*b19, b29*> and

           A28: b = (b19 + b29) by A17, A23, PRE_POLY: 68;

          

           A29: b2 = ( <*b19, b29*> . 2) by A27, A25, FINSEQ_1: 44

          .= b29 by FINSEQ_1: 44;

          

           A30: b1 = ( <*b19, b29*> . 1) by A27, A25, FINSEQ_1: 44

          .= b19 by FINSEQ_1: 44;

           A31:

          now

            assume that

             A32: (p . b1) <> ( 0. L) and

             A33: (q . b2) <> ( 0. L);

             not b11 < b1 by A4, A32;

            then

             A34: b1 <=' b11 by Lm4;

             not b22 < b2 by A2, A33;

            then

             A35: b2 <=' b22 by Lm4;

             A36:

            now

              assume b1 = b11 & b2 = b22;

              

              then (( decomp b) . k) = <*b11, b22*> by A17, A23, A25, PARTFUN1:def 6

              .= (( decomp b) /. i) by A15, PRE_POLY: 48

              .= (( decomp b) . i) by A14, PARTFUN1:def 6;

              hence contradiction by A14, A17, A23, A24, FUNCT_1:def 4;

            end;

            now

              per cases by A36;

                case

                 A37: b1 <> b11;

                 A38:

                now

                  assume (b1 + b2) = (b11 + b2);

                  then b1 = ((b11 + b2) -' b2) by PRE_POLY: 48;

                  hence contradiction by A37, PRE_POLY: 48;

                end;

                (b11 + b22) <=' (b11 + b2) & (b11 + b2) <=' (b11 + b22) by A28, A30, A29, A34, A35, Lm2;

                hence contradiction by A28, A30, A29, A38, Lm3;

              end;

                case

                 A39: b2 <> b22;

                 A40:

                now

                  assume (b2 + b1) = (b22 + b1);

                  then b2 = ((b22 + b1) -' b1) by PRE_POLY: 48;

                  hence contradiction by A39, PRE_POLY: 48;

                end;

                (b11 + b22) <=' (b22 + b1) & (b22 + b1) <=' (b11 + b22) by A28, A30, A29, A34, A35, Lm2;

                hence contradiction by A28, A30, A29, A40, Lm3;

              end;

            end;

            hence contradiction;

          end;

          now

            per cases by A31;

              case (p . b1) = ( 0. L);

              hence ((p . b1) * (q . b2)) = ( 0. L);

            end;

              case (q . b2) = ( 0. L);

              hence ((p . b1) * (q . b2)) = ( 0. L);

            end;

          end;

          hence (s /. k) = ( 0. L) by A26;

        end;

        b1 = ( <*b11, b22*> . 1) by A16, A19, FINSEQ_1: 44

        .= b11 by FINSEQ_1: 44;

        then ((p *' q) . b) = ((p . b11) * (q . b22)) by A5, A18, A22, A20, A21, POLYNOM2: 3;

        then b in ( Support (p *' q)) by A8, POLYNOM1:def 4;

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

        hence thesis;

      end;

    end

    begin

    theorem :: POLYRED:1

    

     Th1: for X be set, L be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, p,q be Series of X, L holds ( - (p + q)) = (( - p) + ( - q))

    proof

      let n be set, L be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, p,q be Series of n, L;

       A1:

      now

        let x be object;

        assume x in ( dom ( - (p + q)));

        then

        reconsider b = x as bag of n;

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

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

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

        .= ( - ((q . b) + (p . b))) by RLVECT_1: 31

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

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

        hence (( - (p + q)) . x) = ((( - p) + ( - q)) . x);

      end;

      ( dom ( - (p + q))) = ( Bags n) by FUNCT_2:def 1

      .= ( dom (( - p) + ( - q))) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: POLYRED:2

    

     Th2: for X be set, L be left_zeroed non empty addLoopStr, p be Series of X, L holds (( 0_ (X,L)) + p) = p

    proof

      let n be set, L be left_zeroed non empty addLoopStr, p be Series of n, L;

      reconsider ls = (( 0_ (n,L)) + p), p9 = p as Function of ( Bags n), the carrier of L;

      now

        let b be Element of ( Bags n);

        

        thus (ls . b) = ((( 0_ (n,L)) . b) + (p . b)) by POLYNOM1: 15

        .= (( 0. L) + (p9 . b)) by POLYNOM1: 22

        .= (p9 . b) by ALGSTR_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: POLYRED:3

    

     Th3: for X be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of X, L holds (( - p) + p) = ( 0_ (X,L)) & (p + ( - p)) = ( 0_ (X,L))

    proof

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

      set q = (( - p) + p);

      now

        let b be Element of ( Bags n);

        

        thus (q . b) = ((( - p) . b) + (p . b)) by POLYNOM1: 15

        .= (( - (p . b)) + (p . b)) by POLYNOM1: 17

        .= ( 0. L) by RLVECT_1: 5

        .= (( 0_ (n,L)) . b) by POLYNOM1: 22;

      end;

      hence (( - p) + p) = ( 0_ (n,L)) by FUNCT_2: 63;

      set q = (p + ( - p));

      now

        let b be Element of ( Bags n);

        

        thus (q . b) = ((p . b) + (( - p) . b)) by POLYNOM1: 15

        .= ((p . b) + ( - (p . b))) by POLYNOM1: 17

        .= ( 0. L) by RLVECT_1: 5

        .= (( 0_ (n,L)) . b) by POLYNOM1: 22;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: POLYRED:4

    

     Th4: for n be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L holds (p - ( 0_ (n,L))) = p

    proof

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

      reconsider pp = (p - ( 0_ (n,L))) as Function of ( Bags n), the carrier of L;

      now

        let b be Element of ( Bags n);

        

        thus (pp . b) = ((p + ( - ( 0_ (n,L)))) . b) by POLYNOM1:def 7

        .= ((p . b) + (( - ( 0_ (n,L))) . b)) by POLYNOM1: 15

        .= ((p . b) + ( - (( 0_ (n,L)) . b))) by POLYNOM1: 17

        .= ((p . b) + ( - ( 0. L))) by POLYNOM1: 22

        .= ((p . b) - ( 0. L))

        .= (p . b) by RLVECT_1: 13;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: POLYRED:5

    

     Th5: for n be Ordinal, L be add-associative right_complementable right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p be Series of n, L holds (( 0_ (n,L)) *' p) = ( 0_ (n,L))

    proof

      let n be Ordinal, L be add-associative right_complementable right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p be Series of n, L;

      set Z = ( 0_ (n,L));

      now

        let b be Element of ( Bags n);

        consider s be FinSequence of the carrier of L such that

         A1: ((Z *' p) . b) = ( Sum s) and ( len s) = ( len ( decomp b)) and

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

        now

          let k be Nat;

          assume k in ( dom s);

          then

          consider b1,b2 be bag of n such that (( decomp b) /. k) = <*b1, b2*> and

           A3: (s /. k) = ((Z . b1) * (p . b2)) by A2;

          

          thus (s /. k) = (( 0. L) * (p . b2)) by A3, POLYNOM1: 22

          .= ( 0. L);

        end;

        then ( Sum s) = ( 0. L) by MATRLIN: 11;

        hence ((Z *' p) . b) = (Z . b) by A1, POLYNOM1: 22;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm7: for n be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p be Polynomial of n, L, q be Element of ( Polynom-Ring (n,L)) st p = q holds ( - p) = ( - q)

    proof

      let n be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p be Polynomial of n, L, q be Element of ( Polynom-Ring (n,L));

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

      reconsider x = ( - p) as Element of R by POLYNOM1:def 11;

      reconsider x as Element of R;

      assume p = q;

      

      then (x + q) = (( - p) + p) by POLYNOM1:def 11

      .= ( 0_ (n,L)) by Th3

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

      hence thesis by RLVECT_1: 6;

    end;

    theorem :: POLYRED:6

    

     Th6: for n be Ordinal, L be Abelian right_zeroed add-associative right_complementable well-unital distributive associative commutative non trivial doubleLoopStr, p,q be Polynomial of n, L holds ( - (p *' q)) = (( - p) *' q) & ( - (p *' q)) = (p *' ( - q))

    proof

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

      reconsider p9 = p, q9 = q as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider p9, q9 as Element of ( Polynom-Ring (n,L));

      

       A1: (p9 * q9) = (p *' q) by POLYNOM1:def 11;

      ( - p) = ( - p9) by Lm7;

      then

       A2: (( - p9) * q9) = (( - p) *' q) by POLYNOM1:def 11;

      ( - q) = ( - q9) by Lm7;

      then

       A3: (p9 * ( - q9)) = (p *' ( - q)) by POLYNOM1:def 11;

      ( - (p9 * q9)) = (( - p9) * q9) & ( - (p9 * q9)) = (p9 * ( - q9)) by VECTSP_1: 9;

      hence thesis by A2, A3, A1, Lm7;

    end;

    

     Lm8: for n be Ordinal, L be add-associative right_complementable right_zeroed non empty addLoopStr, p be Polynomial of n, L, m be Monomial of n, L, b be bag of n st b <> ( term m) holds (m . b) = ( 0. L)

    proof

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

      assume

       A1: b <> ( term m);

      per cases by POLYNOM7: 7;

        suppose ( Support m) = {} ;

        then m = ( 0_ (n,L)) by POLYNOM7: 1;

        hence thesis by POLYNOM1: 22;

      end;

        suppose

         A2: ( Support m) = {( term m)};

        

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

         not b in ( Support m) by A1, A2, TARSKI:def 1;

        hence thesis by A3, POLYNOM1:def 4;

      end;

    end;

    theorem :: POLYRED:7

    

     Th7: for n be Ordinal, L be add-associative right_complementable right_zeroed distributive non empty doubleLoopStr, p be Polynomial of n, L, m be Monomial of n, L, b be bag of n holds ((m *' p) . (( term m) + b)) = ((m . ( term m)) * (p . b))

    proof

      let n be Ordinal, L be add-associative right_complementable right_zeroed distributive non empty doubleLoopStr, p be Polynomial of n, L, m be Monomial of n, L, b2 be bag of n;

      set q = (m *' p), b = (( term m) + b2);

      consider s be FinSequence of the carrier of L such that

       A1: (q . b) = ( Sum s) and

       A2: ( len s) = ( len ( decomp b)) and

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

      consider k be Element of NAT such that

       A4: k in ( dom ( decomp b)) and

       A5: (( decomp (( term m) + b2)) /. k) = <*( term m), b2*> by PRE_POLY: 69;

      

       A6: ( dom s) = ( Seg ( len s)) by FINSEQ_1:def 3

      .= ( dom ( decomp (( term m) + b2))) by A2, FINSEQ_1:def 3;

      then

      consider b19,b29 be bag of n such that

       A7: (( decomp (( term m) + b2)) /. k) = <*b19, b29*> and

       A8: (s /. k) = ((m . b19) * (p . b29)) by A3, A4;

      

       A9: b2 = ( <*( term m), b2*> . 2) by FINSEQ_1: 44

      .= b29 by A5, A7, FINSEQ_1: 44;

      

       A10: for k9 be Element of NAT st k9 in ( dom s) & k9 <> k holds (s /. k9) = ( 0. L)

      proof

        let k9 be Element of NAT ;

        assume that

         A11: k9 in ( dom s) and

         A12: k9 <> k;

        consider b19,b29 be bag of n such that

         A13: (( decomp (( term m) + b2)) /. k9) = <*b19, b29*> and

         A14: (s /. k9) = ((m . b19) * (p . b29)) by A3, A11;

        

         A15: b19 = (( divisors b) /. k9) by A6, A11, A13, PRE_POLY: 70;

        

         A16: (b -' b19) = ( <*b19, (b -' b19)*> . 2) by FINSEQ_1: 44

        .= ( <*b19, b29*> . 2) by A6, A11, A13, A15, PRE_POLY:def 17

        .= b29 by FINSEQ_1: 44;

        per cases ;

          suppose

           A17: b19 = ( term m) & b29 = b2;

          (( decomp (( term m) + b2)) . k9) = (( decomp (( term m) + b2)) /. k9) by A6, A11, PARTFUN1:def 6

          .= (( decomp (( term m) + b2)) . k) by A4, A5, A13, A17, PARTFUN1:def 6;

          hence thesis by A6, A4, A11, A12, FUNCT_1:def 4;

        end;

          suppose b19 <> ( term m);

          then (m . b19) = ( 0. L) by Lm8;

          hence thesis by A14;

        end;

          suppose b29 <> b2;

          then b19 <> ( term m) by A16, PRE_POLY: 48;

          then (m . b19) = ( 0. L) by Lm8;

          hence thesis by A14;

        end;

      end;

      ( term m) = ( <*b19, b29*> . 1) by A5, A7, FINSEQ_1: 44

      .= b19 by FINSEQ_1: 44;

      hence thesis by A1, A6, A4, A8, A9, A10, POLYNOM2: 3;

    end;

    theorem :: POLYRED:8

    

     Th8: for X be set, L be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p be Series of X, L holds (( 0. L) * p) = ( 0_ (X,L))

    proof

      let n be set, L be right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p be Series of n, L;

      set op = (( 0. L) * p);

       A1:

      now

        let u be object;

        assume u in ( dom op);

        then

        reconsider u9 = u as bag of n;

        (op . u9) = (( 0. L) * (p . u9)) by POLYNOM7:def 9

        .= ( 0. L) by BINOM: 1;

        hence (op . u) = (( 0_ (n,L)) . u) by POLYNOM1: 22;

      end;

      ( dom op) = ( Bags n) by FUNCT_2:def 1

      .= ( dom ( 0_ (n,L))) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: POLYRED:9

    

     Th9: for X be set, L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Series of X, L, a be Element of L holds ( - (a * p)) = (( - a) * p) & ( - (a * p)) = (a * ( - p))

    proof

      let n be set, L be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, p be Series of n, L, a be Element of L;

      set ap = (a * p);

       A1:

      now

        let u be object;

        assume u in ( dom ( - ap));

        then

        reconsider u9 = u as bag of n;

        (( - ap) . u9) = ( - (ap . u9)) by POLYNOM1: 17

        .= ( - (a * (p . u9))) by POLYNOM7:def 9

        .= (( - a) * (p . u9)) by VECTSP_1: 9

        .= ((( - a) * p) . u9) by POLYNOM7:def 9;

        hence (( - ap) . u) = ((( - a) * p) . u);

      end;

      ( dom ( - ap)) = ( Bags n) by FUNCT_2:def 1

      .= ( dom (( - a) * p)) by FUNCT_2:def 1;

      hence ( - (a * p)) = (( - a) * p) by A1, FUNCT_1: 2;

       A2:

      now

        let u be object;

        assume u in ( dom ( - ap));

        then

        reconsider u9 = u as bag of n;

        (( - ap) . u9) = ( - (ap . u9)) by POLYNOM1: 17

        .= ( - (a * (p . u9))) by POLYNOM7:def 9

        .= (a * ( - (p . u9))) by VECTSP_1: 8

        .= (a * (( - p) . u9)) by POLYNOM1: 17

        .= ((a * ( - p)) . u9) by POLYNOM7:def 9;

        hence (( - ap) . u) = ((a * ( - p)) . u);

      end;

      ( dom ( - ap)) = ( Bags n) by FUNCT_2:def 1

      .= ( dom (a * ( - p))) by FUNCT_2:def 1;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: POLYRED:10

    

     Th10: for X be set, L be left-distributive non empty doubleLoopStr, p be Series of X, L, a,a9 be Element of L holds ((a * p) + (a9 * p)) = ((a + a9) * p)

    proof

      let n be set, L be left-distributive non empty doubleLoopStr, p be Series of n, L, a,a9 be Element of L;

      set p1 = ((a * p) + (a9 * p)), p2 = ((a + a9) * p);

       A1:

      now

        let u be object;

        assume u in ( dom p1);

        then

        reconsider u9 = u as bag of n;

        (p1 . u9) = (((a * p) . u9) + ((a9 * p) . u9)) by POLYNOM1: 15

        .= ((a * (p . u9)) + ((a9 * p) . u9)) by POLYNOM7:def 9

        .= ((a * (p . u9)) + (a9 * (p . u9))) by POLYNOM7:def 9

        .= ((a + a9) * (p . u9)) by VECTSP_1:def 3

        .= (p2 . u9) by POLYNOM7:def 9;

        hence (p1 . u) = (p2 . u);

      end;

      ( dom p1) = ( Bags n) by FUNCT_2:def 1

      .= ( dom p2) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: POLYRED:11

    

     Th11: for X be set, L be associative non empty multLoopStr_0, p be Series of X, L, a,a9 be Element of L holds ((a * a9) * p) = (a * (a9 * p))

    proof

      let n be set, L be associative non empty multLoopStr_0, p be Series of n, L, a,a9 be Element of L;

      set q = ((a * a9) * p), r = (a * (a9 * p));

       A1:

      now

        let u be object;

        assume u in ( dom q);

        then

        reconsider b = u as bag of n;

        (q . b) = ((a * a9) * (p . b)) by POLYNOM7:def 9

        .= (a * (a9 * (p . b))) by GROUP_1:def 3

        .= (a * ((a9 * p) . b)) by POLYNOM7:def 9

        .= (r . b) by POLYNOM7:def 9;

        hence (q . u) = (r . u);

      end;

      ( dom q) = ( Bags n) by FUNCT_2:def 1

      .= ( dom r) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: POLYRED:12

    

     Th12: for n be Ordinal, L be add-associative right_zeroed right_complementable well-unital associative commutative distributive non empty doubleLoopStr, p,p9 be Series of n, L, a be Element of L holds (a * (p *' p9)) = (p *' (a * p9))

    proof

      let n be Ordinal, L be add-associative right_zeroed right_complementable well-unital commutative associative distributive non empty doubleLoopStr, p,p9 be Series of n, L, a be Element of L;

      set app = (a * (p *' p9)), pap = (p *' (a * p9)), pp = (p *' p9);

       A1:

      now

        let u be object;

        assume u in ( dom app);

        then

        reconsider b = u as bag of n;

        consider s be FinSequence of the carrier of L such that

         A2: (pap . b) = ( Sum s) and

         A3: ( len s) = ( len ( decomp b)) and

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

        consider t be FinSequence of the carrier of L such that

         A5: (pp . b) = ( Sum t) and

         A6: ( len t) = ( len ( decomp b)) and

         A7: for k be Element of NAT st k in ( dom t) holds ex b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (t /. k) = ((p . b1) * (p9 . b2)) by POLYNOM1:def 10;

        

         A8: ( dom t) = ( Seg ( len s)) by A3, A6, FINSEQ_1:def 3

        .= ( dom s) by FINSEQ_1:def 3;

        now

          let i be object;

          assume

           A9: i in ( dom t);

          then

          reconsider k = i as Element of NAT ;

          consider b1,b2 be bag of n such that

           A10: (( decomp b) /. k) = <*b1, b2*> and

           A11: (t /. k) = ((p . b1) * (p9 . b2)) by A7, A9;

          consider a1,a2 be bag of n such that

           A12: (( decomp b) /. k) = <*a1, a2*> and

           A13: (s /. k) = ((p . a1) * ((a * p9) . a2)) by A4, A8, A9;

          

           A14: b2 = ( <*a1, a2*> . 2) by A10, A12, FINSEQ_1: 44

          .= a2 by FINSEQ_1: 44;

          b1 = ( <*a1, a2*> . 1) by A10, A12, FINSEQ_1: 44

          .= a1 by FINSEQ_1: 44;

          

          hence (s /. i) = ((p . b1) * (a * (p9 . b2))) by A13, A14, POLYNOM7:def 9

          .= (a * (t /. i)) by A11, GROUP_1:def 3;

        end;

        then s = (a * t) by A8, POLYNOM1:def 1;

        

        then (pap . b) = (a * ( Sum t)) by A2, POLYNOM1: 12

        .= (app . b) by A5, POLYNOM7:def 9;

        hence (app . u) = (pap . u);

      end;

      ( dom app) = ( Bags n) by FUNCT_2:def 1

      .= ( dom pap) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    begin

    definition

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

      :: POLYRED:def1

      func b *' p -> Series of n, L means

      : Def1: for b9 be bag of n st b divides b9 holds (it . b9) = (p . (b9 -' b)) & for b9 be bag of n st not b divides b9 holds (it . b9) = ( 0. L);

      existence

      proof

        set M1 = { [b9, (p . (b9 -' b))] where b9 be Element of ( Bags n) : b divides b9 }, M2 = { [b9, ( 0. L)] where b9 be Element of ( Bags n) : not (b divides b9) };

        set M = (M1 \/ M2);

        now

          let u be object;

          assume

           A1: u in M;

          now

            per cases by A1, XBOOLE_0:def 3;

              case u in M1;

              then ex b9 be Element of ( Bags n) st u = [b9, (p . (b9 -' b))] & b divides b9;

              hence u in [:( Bags n), the carrier of L:] by ZFMISC_1:def 2;

            end;

              case u in M2;

              then ex b9 be Element of ( Bags n) st u = [b9, ( 0. L)] & not b divides b9;

              hence u in [:( Bags n), the carrier of L:] by ZFMISC_1:def 2;

            end;

          end;

          hence u in [:( Bags n), the carrier of L:];

        end;

        then

        reconsider M as Relation of ( Bags n), the carrier of L by TARSKI:def 3;

         A2:

        now

          let u be object;

          assume u in ( Bags n);

          then

          reconsider u9 = u as bag of n;

          

           A3: u9 is Element of ( Bags n) by PRE_POLY:def 12;

          now

            per cases ;

              case not b divides u9;

              then [u9, ( 0. L)] in { [b9, ( 0. L)] where b9 be Element of ( Bags n) : not (b divides b9) } by A3;

              then [u9, ( 0. L)] in M by XBOOLE_0:def 3;

              hence u in ( dom M) by XTUPLE_0:def 12;

            end;

              case b divides u9;

              then [u9, (p . (u9 -' b))] in { [b9, (p . (b9 -' b))] where b9 be Element of ( Bags n) : b divides b9 } by A3;

              then [u9, (p . (u9 -' b))] in M by XBOOLE_0:def 3;

              hence u in ( dom M) by XTUPLE_0:def 12;

            end;

          end;

          hence u in ( dom M);

        end;

        for u be object holds u in ( dom M) implies u in ( Bags n);

        then

         A4: ( dom M) = ( Bags n) by A2, TARSKI: 2;

         A5:

        now

          let x,y1,y2 be object;

          assume

           A6: [x, y1] in M & [x, y2] in M;

           A7:

          now

            assume that

             A8: [x, y1] in M2 and

             A9: [x, y2] in M1;

            consider v be Element of ( Bags n) such that

             A10: [v, ( 0. L)] = [x, y1] and

             A11: not b divides v by A8;

            consider u be Element of ( Bags n) such that

             A12: [u, (p . (u -' b))] = [x, y2] and

             A13: b divides u by A9;

            u = x by A12, XTUPLE_0: 1

            .= v by A10, XTUPLE_0: 1;

            hence contradiction by A13, A11;

          end;

           A14:

          now

            assume that

             A15: [x, y1] in M1 and

             A16: [x, y2] in M2;

            consider v be Element of ( Bags n) such that

             A17: [v, ( 0. L)] = [x, y2] and

             A18: not b divides v by A16;

            consider u be Element of ( Bags n) such that

             A19: [u, (p . (u -' b))] = [x, y1] and

             A20: b divides u by A15;

            u = x by A19, XTUPLE_0: 1

            .= v by A17, XTUPLE_0: 1;

            hence contradiction by A20, A18;

          end;

          thus [x, y1] in M1 & [x, y2] in M1 or [x, y1] in M2 & [x, y2] in M2

          proof

            assume

             A21: not ( [x, y1] in M1 & [x, y2] in M1);

            now

              per cases by A21;

                case not [x, y1] in M1;

                hence thesis by A6, A7, XBOOLE_0:def 3;

              end;

                case not [x, y2] in M1;

                hence thesis by A6, A14, XBOOLE_0:def 3;

              end;

            end;

            hence thesis;

          end;

        end;

        now

          let x,y1,y2 be object;

          assume

           A22: [x, y1] in M & [x, y2] in M;

          now

            per cases by A5, A22;

              case

               A23: [x, y1] in M1 & [x, y2] in M1;

              then

              consider v be Element of ( Bags n) such that

               A24: [v, (p . (v -' b))] = [x, y2] and b divides v;

              consider u be Element of ( Bags n) such that

               A25: [u, (p . (u -' b))] = [x, y1] and b divides u by A23;

              u = x by A25, XTUPLE_0: 1

              .= v by A24, XTUPLE_0: 1;

              

              hence y1 = (p . (v -' b)) by A25, XTUPLE_0: 1

              .= y2 by A24, XTUPLE_0: 1;

            end;

              case

               A26: [x, y1] in M2 & [x, y2] in M2;

              then

               A27: ex v be Element of ( Bags n) st [v, ( 0. L)] = [x, y2] & not b divides v;

              

               A28: ex u be Element of ( Bags n) st [u, ( 0. L)] = [x, y1] & not b divides u by A26;

              

              thus y1 = ( 0. L) by A28, XTUPLE_0: 1

              .= y2 by A27, XTUPLE_0: 1;

            end;

          end;

          hence y1 = y2;

        end;

        then

        reconsider M as Function of ( Bags n), the carrier of L by A4, FUNCT_1:def 1, FUNCT_2:def 1;

        reconsider M as Function of ( Bags n), L;

        take M;

         A29:

        now

          let b9 be bag of n;

          

           A30: b9 is Element of ( Bags n) by PRE_POLY:def 12;

          assume not b divides b9;

          then [b9, ( 0. L)] in { [u, ( 0. L)] where u be Element of ( Bags n) : not (b divides u) } by A30;

          then [b9, ( 0. L)] in M by XBOOLE_0:def 3;

          hence (M . b9) = ( 0. L) by FUNCT_1: 1;

        end;

        now

          let b9 be bag of n;

          

           A31: b9 is Element of ( Bags n) by PRE_POLY:def 12;

          assume b divides b9;

          then [b9, (p . (b9 -' b))] in { [u, (p . (u -' b))] where u be Element of ( Bags n) : b divides u } by A31;

          then [b9, (p . (b9 -' b))] in M by XBOOLE_0:def 3;

          hence (M . b9) = (p . (b9 -' b)) by FUNCT_1: 1;

        end;

        hence thesis by A29;

      end;

      uniqueness

      proof

        let p1,p2 be Series of n, L such that

         A32: for b9 be bag of n st b divides b9 holds (p1 . b9) = (p . (b9 -' b)) & for b9 be bag of n st not b divides b9 holds (p1 . b9) = ( 0. L) and

         A33: for b9 be bag of n st b divides b9 holds (p2 . b9) = (p . (b9 -' b)) & for b9 be bag of n st not b divides b9 holds (p2 . b9) = ( 0. L);

        now

          let x be Element of ( Bags n);

          now

            per cases ;

              case

               A34: b divides x;

              

              hence (p1 . x) = (p . (x -' b)) by A32

              .= (p2 . x) by A33, A34;

            end;

              case

               A35: not b divides x;

              

              hence (p1 . x) = ( 0. L) by A32

              .= (p2 . x) by A33, A35;

            end;

          end;

          hence (p1 . x) = (p2 . x);

        end;

        hence p1 = p2 by FUNCT_2: 63;

      end;

    end

    

     Lm9: for n be Ordinal, b,b9 be bag of n, L be non empty ZeroStr, p be Series of n, L holds ((b *' p) . (b9 + b)) = (p . b9)

    proof

      let n be Ordinal, b,b9 be bag of n, L be non empty ZeroStr, p be Series of n, L;

      b divides (b9 + b) by PRE_POLY: 50;

      

      hence ((b *' p) . (b9 + b)) = (p . ((b9 + b) -' b)) by Def1

      .= (p . b9) by PRE_POLY: 48;

    end;

    

     Lm10: for n be Ordinal, L be non empty ZeroStr, p be Polynomial of n, L, b be bag of n holds ( Support (b *' p)) c= { (b + b9) where b9 be Element of ( Bags n) : b9 in ( Support p) }

    proof

      let n be Ordinal, L be non empty ZeroStr, p be Polynomial of n, L, b be bag of n;

      now

        let u be object;

        assume

         A1: u in ( Support (b *' p));

        then

        reconsider u9 = u as Element of ( Bags n);

        

         A2: ((b *' p) . u9) <> ( 0. L) by A1, POLYNOM1:def 4;

        then b divides u9 by Def1;

        then

        consider s be bag of n such that

         A3: u9 = (b + s) by TERMORD: 1;

        s is Element of ( Bags n) & (p . s) <> ( 0. L) by A2, A3, Lm9, PRE_POLY:def 12;

        then s in ( Support p) by POLYNOM1:def 4;

        hence u in { (b + b9) where b9 be Element of ( Bags n) : b9 in ( Support p) } by A3;

      end;

      hence thesis by TARSKI:def 3;

    end;

    registration

      let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be finite-Support Series of n, L;

      cluster (b *' p) -> finite-Support;

      coherence

      proof

        set f = { [b9, (b + b9)] where b9 be Element of ( Bags n) : b9 in ( Support p) };

         A1:

        now

          let u be object;

          assume u in f;

          then ex b9 be Element of ( Bags n) st u = [b9, (b + b9)] & b9 in ( Support p);

          hence ex y,z be object st u = [y, z];

        end;

        now

          let x,y1,y2 be object;

          assume that

           A2: [x, y1] in f and

           A3: [x, y2] in f;

          consider b2 be Element of ( Bags n) such that

           A4: [x, y2] = [b2, (b + b2)] and b2 in ( Support p) by A3;

          consider b1 be Element of ( Bags n) such that

           A5: [x, y1] = [b1, (b + b1)] and b1 in ( Support p) by A2;

          b1 = x by A5, XTUPLE_0: 1

          .= b2 by A4, XTUPLE_0: 1;

          hence y1 = y2 by A5, A4, XTUPLE_0: 1;

        end;

        then

        reconsider f as Function by A1, FUNCT_1:def 1, RELAT_1:def 1;

         A6:

        now

          let u be object;

          assume u in ( dom f);

          then

          consider v be object such that

           A7: [u, v] in f by XTUPLE_0:def 12;

          consider b9 be Element of ( Bags n) such that

           A8: [u, v] = [b9, (b + b9)] and

           A9: b9 in ( Support p) by A7;

          u = b9 by A8, XTUPLE_0: 1;

          hence u in ( Support p) by A9;

        end;

        

         A10: ( Support (b *' p)) c= { (b + b9) where b9 be Element of ( Bags n) : b9 in ( Support p) } by Lm10;

        now

          let u be object;

          assume u in ( Support (b *' p));

          then u in { (b + b9) where b9 be Element of ( Bags n) : b9 in ( Support p) } by A10;

          then

          consider b9 be Element of ( Bags n) such that

           A11: u = (b + b9) & b9 in ( Support p);

           [b9, u] in f by A11;

          hence u in ( rng f) by XTUPLE_0:def 13;

        end;

        then

         A12: ( Support (b *' p)) c= ( rng f) by TARSKI:def 3;

        now

          let u be object;

          assume

           A13: u in ( Support p);

          then

          reconsider u9 = u as Element of ( Bags n);

           [u9, (b + u9)] in { [b9, (b + b9)] where b9 be Element of ( Bags n) : b9 in ( Support p) } by A13;

          hence u in ( dom f) by XTUPLE_0:def 12;

        end;

        then ( dom f) = ( Support p) by A6, TARSKI: 2;

        then ( dom f) is finite by POLYNOM1:def 5;

        then ( rng f) is finite by FINSET_1: 8;

        hence thesis by A12, POLYNOM1:def 5;

      end;

    end

    theorem :: POLYRED:13

    for n be Ordinal, b,b9 be bag of n, L be non empty ZeroStr, p be Series of n, L holds ((b *' p) . (b9 + b)) = (p . b9) by Lm9;

    theorem :: POLYRED:14

    for n be Ordinal, L be non empty ZeroStr, p be Polynomial of n, L, b be bag of n holds ( Support (b *' p)) c= { (b + b9) where b9 be Element of ( Bags n) : b9 in ( Support p) } by Lm10;

    theorem :: POLYRED:15

    

     Th15: for n be Ordinal, T be connected admissible TermOrder of n, L be non trivial ZeroStr, p be non-zero Polynomial of n, L, b be bag of n holds ( HT ((b *' p),T)) = (b + ( HT (p,T)))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be non trivial ZeroStr, p be non-zero Polynomial of n, L, b be bag of n;

      set htp = ( HT (p,T));

      per cases ;

        suppose

         A1: ( Support (b *' p)) = {} ;

        now

          assume ( Support p) <> {} ;

          then

          reconsider sp = ( Support p) as non empty set;

          set u = the Element of sp;

          u in ( Support p);

          then

          reconsider u9 = u as Element of ( Bags n);

          b divides (b + u9) by PRE_POLY: 50;

          

          then ((b *' p) . (b + u9)) = (p . ((b + u9) -' b)) by Def1

          .= (p . u9) by PRE_POLY: 48;

          then

           A2: ((b *' p) . (b + u9)) <> ( 0. L) by POLYNOM1:def 4;

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

          hence contradiction by A1, A2, POLYNOM1:def 4;

        end;

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

        hence thesis by POLYNOM7:def 1;

      end;

        suppose

         A3: ( Support (b *' p)) <> {} ;

        now

          reconsider sp = ( Support (b *' p)) as non empty set by A3;

          set u = the Element of sp;

          u in ( Support (b *' p));

          then

          reconsider u9 = u as Element of ( Bags n);

          

           A4: (u9 -' b) is Element of ( Bags n) by PRE_POLY:def 12;

          

           A5: ((b *' p) . u9) <> ( 0. L) by POLYNOM1:def 4;

          then b divides u9 by Def1;

          then

           A6: (p . (u9 -' b)) <> ( 0. L) by A5, Def1;

          assume ( Support p) = {} ;

          hence contradiction by A6, A4, POLYNOM1:def 4;

        end;

        then htp in ( Support p) by TERMORD:def 6;

        then

         A7: (p . htp) <> ( 0. L) by POLYNOM1:def 4;

         A8:

        now

          let b9 be bag of n;

          assume b9 in ( Support (b *' p));

          then

           A9: ((b *' p) . b9) <> ( 0. L) by POLYNOM1:def 4;

          then b divides b9 by Def1;

          then

          consider b3 be bag of n such that

           A10: (b + b3) = b9 by TERMORD: 1;

          

           A11: b3 is Element of ( Bags n) by PRE_POLY:def 12;

          ((b *' p) . b9) = (p . b3) by A10, Lm9;

          then b3 in ( Support p) by A9, A11, POLYNOM1:def 4;

          then b3 <= (htp,T) by TERMORD:def 6;

          then [b3, htp] in T by TERMORD:def 2;

          then [b9, (b + htp)] in T by A10, BAGORDER:def 5;

          hence b9 <= ((b + htp),T) by TERMORD:def 2;

        end;

        ((b *' p) . (b + htp)) = (p . htp) & (b + htp) is Element of ( Bags n) by Lm9, PRE_POLY:def 12;

        then (b + htp) in ( Support (b *' p)) by A7, POLYNOM1:def 4;

        hence thesis by A8, TERMORD:def 6;

      end;

    end;

    theorem :: POLYRED:16

    

     Th16: for n be Ordinal, T be connected admissible TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L, b,b9 be bag of n holds b9 in ( Support (b *' p)) implies b9 <= ((b + ( HT (p,T))),T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L, b,b9 be bag of n;

      assume

       A1: b9 in ( Support (b *' p));

      ( Support (b *' p)) c= { (b + b2) where b2 be Element of ( Bags n) : b2 in ( Support p) } by Lm10;

      then b9 in { (b + b2) where b2 be Element of ( Bags n) : b2 in ( Support p) } by A1;

      then

      consider s be Element of ( Bags n) such that

       A2: b9 = (b + s) and

       A3: s in ( Support p);

      s <= (( HT (p,T)),T) by A3, TERMORD:def 6;

      then [s, ( HT (p,T))] in T by TERMORD:def 2;

      then [(b + s), (b + ( HT (p,T)))] in T by BAGORDER:def 5;

      hence thesis by A2, TERMORD:def 2;

    end;

    theorem :: POLYRED:17

    for n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Series of n, L holds (( EmptyBag n) *' p) = p

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Series of n, L;

      set e = ( EmptyBag n);

       A1:

      now

        let u be object;

        assume u in ( dom p);

        then

        reconsider u9 = u as Element of ( Bags n);

        ( EmptyBag n) divides u9 by PRE_POLY: 59;

        

        then ((e *' p) . u9) = (p . (u9 -' e)) by Def1

        .= (p . u9) by PRE_POLY: 54;

        hence ((e *' p) . u) = (p . u);

      end;

      ( dom (e *' p)) = ( Bags n) by FUNCT_2:def 1

      .= ( dom p) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: POLYRED:18

    

     Th18: for n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Series of n, L, b1,b2 be bag of n holds ((b1 + b2) *' p) = (b1 *' (b2 *' p))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Series of n, L, b1,b2 be bag of n;

      set q = ((b1 + b2) *' p), r = (b1 *' (b2 *' p));

       A1:

      now

        let u be object;

        assume u in ( dom q);

        then

        reconsider b = u as bag of n;

        now

          per cases ;

            case

             A2: (b1 + b2) divides b;

            then

            consider b3 be bag of n such that

             A3: ((b1 + b2) + b3) = b by TERMORD: 1;

            

             A4: (b1 + (b2 + b3)) = b by A3, PRE_POLY: 35;

            then (b2 + b3) = (b -' b1) by PRE_POLY: 48;

            then

             A5: b2 divides (b -' b1) by TERMORD: 1;

            b1 divides b by A4, TERMORD: 1;

            then (r . b) = ((b2 *' p) . (b -' b1)) by Def1;

            

            hence (r . b) = (p . ((b -' b1) -' b2)) by A5, Def1

            .= (p . (b -' (b1 + b2))) by PRE_POLY: 36

            .= (q . b) by A2, Def1;

          end;

            case

             A6: not (b1 + b2) divides b;

            then

             A7: (q . b) = ( 0. L) by Def1;

            now

              per cases ;

                case

                 A8: b1 divides b;

                 A9:

                now

                  assume b2 divides (b -' b1);

                  then (((b -' b1) -' b2) + b2) = (b -' b1) by PRE_POLY: 47;

                  then ((((b -' b1) -' b2) + b2) + b1) = b by A8, PRE_POLY: 47;

                  then (((b -' b1) -' b2) + (b2 + b1)) = b by PRE_POLY: 35;

                  hence contradiction by A6, TERMORD: 1;

                end;

                (r . b) = ((b2 *' p) . (b -' b1)) by A8, Def1;

                hence (q . b) = (r . b) by A7, A9, Def1;

              end;

                case not b1 divides b;

                hence (q . b) = (r . b) by A7, Def1;

              end;

            end;

            hence (q . b) = (r . b);

          end;

        end;

        hence (q . u) = (r . u);

      end;

      ( dom q) = ( Bags n) by FUNCT_2:def 1

      .= ( dom r) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: POLYRED:19

    

     Th19: for n be Ordinal, L be add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr, p be Polynomial of n, L, a be Element of L holds ( Support (a * p)) c= ( Support p)

    proof

      let n be Ordinal, L be add-associative right_zeroed right_complementable distributive non trivial doubleLoopStr, p be Polynomial of n, L, a9 be Element of L;

      

       A1: ( dom ( 0_ (n,L))) = ( Bags n) by FUNCT_2:def 1

      .= ( dom (a9 * p)) by FUNCT_2:def 1;

      per cases ;

        suppose

         A2: a9 = ( 0. L);

        now

          let u be object;

          assume u in ( dom (a9 * p));

          then

          reconsider u9 = u as Element of ( Bags n);

          ((a9 * p) . u9) = (a9 * (p . u9)) by POLYNOM7:def 9

          .= ( 0. L) by A2

          .= (( 0_ (n,L)) . u9) by POLYNOM1: 22;

          hence ((a9 * p) . u) = (( 0_ (n,L)) . u);

        end;

        then (a9 * p) = ( 0_ (n,L)) by A1, FUNCT_1: 2;

        then for u be object holds u in ( Support (a9 * p)) implies u in ( Support p) by POLYNOM7: 1;

        hence thesis by TARSKI:def 3;

      end;

        suppose a9 <> ( 0. L);

        then

        reconsider a = a9 as non zero Element of L by STRUCT_0:def 12;

        now

          let u be object;

          assume

           A3: u in ( Support (a * p));

          then

          reconsider u9 = u as Element of ( Bags n);

          

           A4: ((a * p) . u9) = (a * (p . u9)) by POLYNOM7:def 9;

          ((a * p) . u9) <> ( 0. L) by A3, POLYNOM1:def 4;

          then (p . u9) <> ( 0. L) by A4;

          hence u in ( Support p) by POLYNOM1:def 4;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end;

    theorem :: POLYRED:20

    for n be Ordinal, L be domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, a be non zero Element of L holds ( Support p) c= ( Support (a * p))

    proof

      let n be Ordinal, L be domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, a be non zero Element of L;

      now

        let u be object;

        assume

         A1: u in ( Support p);

        then

        reconsider u9 = u as Element of ( Bags n);

        

         A2: ((a * p) . u9) = (a * (p . u9)) & a <> ( 0. L) by POLYNOM7:def 9;

        (p . u9) <> ( 0. L) by A1, POLYNOM1:def 4;

        then ((a * p) . u9) <> ( 0. L) by A2, VECTSP_2:def 1;

        hence u in ( Support (a * p)) by POLYNOM1:def 4;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: POLYRED:21

    

     Th21: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, a be non zero Element of L holds ( HT ((a * p),T)) = ( HT (p,T))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, a be non zero Element of L;

      set ht = ( HT ((a * p),T)), htp = ( HT (p,T));

      per cases ;

        suppose

         A1: ( Support (a * p)) = {} ;

        now

          assume ( Support p) <> {} ;

          then

          reconsider sp = ( Support p) as non empty set;

          set u = the Element of sp;

          u in ( Support p);

          then

          reconsider u9 = u as Element of ( Bags n);

          

           A2: ((a * p) . u9) = (a * (p . u9)) by POLYNOM7:def 9;

          (p . u9) <> ( 0. L) & a <> ( 0. L) by POLYNOM1:def 4;

          then ((a * p) . u9) <> ( 0. L) by A2, VECTSP_2:def 1;

          hence contradiction by A1, POLYNOM1:def 4;

        end;

        

        hence htp = ( EmptyBag n) by TERMORD:def 6

        .= ht by A1, TERMORD:def 6;

      end;

        suppose

         A3: ( Support (a * p)) <> {} ;

        now

          reconsider sp = ( Support (a * p)) as non empty set by A3;

          set u = the Element of sp;

          u in ( Support (a * p));

          then

          reconsider u9 = u as Element of ( Bags n);

          ((a * p) . u9) <> ( 0. L) & ((a * p) . u9) = (a * (p . u9)) by POLYNOM1:def 4, POLYNOM7:def 9;

          then

           A4: (p . u9) <> ( 0. L);

          assume ( Support p) = {} ;

          hence contradiction by A4, POLYNOM1:def 4;

        end;

        then htp in ( Support p) by TERMORD:def 6;

        then

         A5: (p . htp) <> ( 0. L) by POLYNOM1:def 4;

         A6:

        now

          let b be bag of n;

          assume

           A7: b in ( Support (a * p));

          ( Support (a * p)) c= ( Support p) by Th19;

          hence b <= (htp,T) by A7, TERMORD:def 6;

        end;

        ((a * p) . htp) = (a * (p . htp)) by POLYNOM7:def 9;

        then ((a * p) . htp) <> ( 0. L) by A5, VECTSP_2:def 1;

        then htp in ( Support (a * p)) by POLYNOM1:def 4;

        hence thesis by A6, TERMORD:def 6;

      end;

    end;

    theorem :: POLYRED:22

    

     Th22: for n be Ordinal, L be add-associative right_complementable right_zeroed distributive non trivial doubleLoopStr, p be Series of n, L, b be bag of n, a be Element of L holds (a * (b *' p)) = (( Monom (a,b)) *' p)

    proof

      let n be Ordinal, L be add-associative right_complementable right_zeroed distributive non trivial doubleLoopStr, p be Series of n, L, b be bag of n, a be Element of L;

      set q = (a * (b *' p)), q9 = (( Monom (a,b)) *' p), m = ( Monom (a,b));

      per cases ;

        suppose a <> ( 0. L);

        then

        reconsider a as non zero Element of L by STRUCT_0:def 12;

         A1:

        now

          let u be object;

          assume u in ( dom q);

          then

          reconsider s = u as bag of n;

          consider t be FinSequence of the carrier of L such that

           A2: (q9 . s) = ( Sum t) and

           A3: ( len t) = ( len ( decomp s)) and

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

          

           A5: ( dom t) = ( Seg ( len ( decomp s))) by A3, FINSEQ_1:def 3

          .= ( dom ( decomp s)) by FINSEQ_1:def 3;

          

           A6: ( term ( Monom (a,b))) = b by POLYNOM7: 10;

          now

            per cases ;

              case

               A7: b divides s;

              

               A8: (q . s) = (a * ((b *' p) . s)) by POLYNOM7:def 9

              .= (a * (p . (s -' b))) by A7, Def1;

              consider s9 be bag of n such that

               A9: (b + s9) = s by A7, TERMORD: 1;

              consider i be Element of NAT such that

               A10: i in ( dom ( decomp s)) and

               A11: (( decomp s) /. i) = <*b, s9*> by A9, PRE_POLY: 69;

              consider b1,b2 be bag of n such that

               A12: (( decomp s) /. i) = <*b1, b2*> and

               A13: (t /. i) = ((m . b1) * (p . b2)) by A4, A5, A10;

              

               A14: b2 = ( <*b, s9*> . 2) by A11, A12, FINSEQ_1: 44

              .= s9 by FINSEQ_1: 44;

              

               A15: (s -' b) = s9 by A9, PRE_POLY: 48;

               A16:

              now

                let i9 be Element of NAT ;

                assume that

                 A17: i9 in ( dom t) and

                 A18: i9 <> i;

                consider b19,b29 be bag of n such that

                 A19: (( decomp s) /. i9) = <*b19, b29*> and

                 A20: (t /. i9) = ((m . b19) * (p . b29)) by A4, A17;

                consider h1,h2 be bag of n such that

                 A21: (( decomp s) /. i9) = <*h1, h2*> and

                 A22: s = (h1 + h2) by A5, A17, PRE_POLY: 68;

                

                 A23: (s -' h1) = h2 by A22, PRE_POLY: 48;

                

                 A24: h1 = ( <*b19, b29*> . 1) by A19, A21, FINSEQ_1: 44

                .= b19 by FINSEQ_1: 44;

                now

                  assume (m . b19) <> ( 0. L);

                  then b19 = b by A6, POLYNOM7:def 5;

                  

                  then (( decomp s) . i9) = (( decomp s) /. i) by A5, A11, A15, A17, A21, A24, A23, PARTFUN1:def 6

                  .= (( decomp s) . i) by A10, PARTFUN1:def 6;

                  hence contradiction by A5, A10, A17, A18, FUNCT_1:def 4;

                end;

                hence (t /. i9) = ( 0. L) by A20;

              end;

              b1 = ( <*b, s9*> . 1) by A11, A12, FINSEQ_1: 44

              .= b by FINSEQ_1: 44;

              

              then ( Sum t) = (( coefficient m) * (p . (s -' b))) by A6, A5, A10, A15, A13, A14, A16, POLYNOM2: 3

              .= (a * (p . (s -' b))) by POLYNOM7: 9;

              hence (q . s) = (q9 . s) by A2, A8;

            end;

              case

               A25: not b divides s;

              consider t be FinSequence of the carrier of L such that

               A26: (q9 . s) = ( Sum t) and

               A27: ( len t) = ( len ( decomp s)) and

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

               A29:

              now

                let k be Nat;

                assume

                 A30: k in ( dom t);

                then

                consider b19,b29 be bag of n such that

                 A31: (( decomp s) /. k) = <*b19, b29*> and

                 A32: (t /. k) = ((m . b19) * (p . b29)) by A28;

                

                 A33: ( dom t) = ( Seg ( len ( decomp s))) by A27, FINSEQ_1:def 3

                .= ( dom ( decomp s)) by FINSEQ_1:def 3;

                now

                  per cases ;

                    case

                     A34: b19 = ( term m);

                    consider h1,h2 be bag of n such that

                     A35: (( decomp s) /. k) = <*h1, h2*> and

                     A36: s = (h1 + h2) by A30, A33, PRE_POLY: 68;

                    h1 = ( <*b19, b29*> . 1) by A31, A35, FINSEQ_1: 44

                    .= b19 by FINSEQ_1: 44;

                    hence contradiction by A6, A25, A34, A36, TERMORD: 1;

                  end;

                    case b19 <> ( term m);

                    hence (m . b19) = ( 0. L) by Lm8;

                  end;

                end;

                hence (t /. k) = ( 0. L) by A32;

              end;

              (q . s) = (a * ((b *' p) . s)) by POLYNOM7:def 9

              .= (a * ( 0. L)) by A25, Def1

              .= ( 0. L);

              hence (q . u) = (q9 . u) by A26, A29, MATRLIN: 11;

            end;

          end;

          hence (q . u) = (q9 . u);

        end;

        ( dom q) = ( Bags n) by FUNCT_2:def 1

        .= ( dom q9) by FUNCT_2:def 1;

        hence thesis by A1, FUNCT_1: 2;

      end;

        suppose

         A37: a = ( 0. L);

         A38:

        now

          let u be object;

          assume u in ( dom m);

          then

          reconsider u9 = u as Element of ( Bags n);

          now

            per cases ;

              case

               A39: u9 = ( term m);

              ( coefficient m) = ( 0. L) by A37, POLYNOM7: 8;

              hence (m . u) = (( 0_ (n,L)) . u) by A39, POLYNOM1: 22;

            end;

              case u9 <> ( term m);

              

              then (m . u9) = ( 0. L) by Lm8

              .= (( 0_ (n,L)) . u9) by POLYNOM1: 22;

              hence (m . u) = (( 0_ (n,L)) . u);

            end;

          end;

          hence (m . u) = (( 0_ (n,L)) . u);

        end;

        ( dom m) = ( Bags n) by FUNCT_2:def 1

        .= ( dom ( 0_ (n,L))) by FUNCT_2:def 1;

        then

         A40: m = ( 0_ (n,L)) by A38, FUNCT_1: 2;

         A41:

        now

          let u be object;

          assume u in ( dom q);

          then

          reconsider u9 = u as bag of n;

          (q . u9) = (( 0. L) * ((b *' p) . u9)) by A37, POLYNOM7:def 9

          .= ( 0. L)

          .= (( 0_ (n,L)) . u9) by POLYNOM1: 22;

          hence (q . u) = (( 0_ (n,L)) . u);

        end;

        ( dom q) = ( Bags n) by FUNCT_2:def 1

        .= ( dom ( 0_ (n,L))) by FUNCT_2:def 1;

        then q = ( 0_ (n,L)) by A41, FUNCT_1: 2;

        hence thesis by A40, Th5;

      end;

    end;

    theorem :: POLYRED:23

    for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be non-zero Polynomial of n, L, q be Polynomial of n, L, m be non-zero Monomial of n, L holds ( HT (p,T)) in ( Support q) implies ( HT ((m *' p),T)) in ( Support (m *' q))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be non-zero Polynomial of n, L, q be Polynomial of n, L, m be non-zero Monomial of n, L;

      set a = ( coefficient m), b = ( term m);

      assume ( HT (p,T)) in ( Support q);

      then

       A1: (q . ( HT (p,T))) <> ( 0. L) by POLYNOM1:def 4;

      

       A2: ( HC (m,T)) <> ( 0. L);

      then

      reconsider a as non zero Element of L by TERMORD: 23;

      m = ( Monom (a,b)) by POLYNOM7: 11;

      then (m *' p) = (a * (b *' p)) by Th22;

      

      then ( HT ((m *' p),T)) = ( HT ((b *' p),T)) by Th21

      .= (b + ( HT (p,T))) by Th15;

      then

       A3: ((m *' q) . ( HT ((m *' p),T))) = ((m . ( term m)) * (q . ( HT (p,T)))) by Th7;

      (m . ( HT (m,T))) <> ( 0. L) by A2, TERMORD:def 7;

      then (m . ( term m)) <> ( 0. L) by POLYNOM7:def 5;

      then ((m *' q) . ( HT ((m *' p),T))) <> ( 0. L) by A1, A3, VECTSP_2:def 1;

      hence thesis by POLYNOM1:def 4;

    end;

    begin

    registration

      let n be Ordinal, T be connected TermOrder of n;

      cluster RelStr (# ( Bags n), T #) -> connected;

      coherence

      proof

        set L = RelStr (# ( Bags n), T #);

        now

          let x,y be Element of L;

          reconsider x9 = x as bag of n;

          reconsider y9 = y as bag of n;

          y9 <= (y9,T) by TERMORD: 6;

          then [y9, y9] in T by TERMORD:def 2;

          then

           A1: y in ( field T) by RELAT_1: 15;

          x9 <= (x9,T) by TERMORD: 6;

          then [x9, x9] in T by TERMORD:def 2;

          then

           A2: T is_connected_in ( field T) & x in ( field T) by RELAT_1: 15, RELAT_2:def 14;

          now

            per cases ;

              case x <> y;

              then [x, y] in the InternalRel of L or [y, x] in the InternalRel of L by A2, A1, RELAT_2:def 6;

              hence x <= y or y <= x by ORDERS_2:def 5;

            end;

              case x = y;

              then x9 <= (y9,T) by TERMORD: 6;

              then [x9, y9] in the InternalRel of L by TERMORD:def 2;

              hence x <= y or y <= x by ORDERS_2:def 5;

            end;

          end;

          hence x <= y or y <= x;

        end;

        hence thesis by WAYBEL_0:def 29;

      end;

    end

    registration

      let n be Nat, T be admissible TermOrder of n;

      cluster RelStr (# ( Bags n), T #) -> well_founded;

      coherence

      proof

        set R = RelStr (# ( Bags n), T #), X = the carrier of R;

        now

          let Y be set;

          assume that

           A1: Y c= X and

           A2: Y <> {} ;

          now

            let u be object;

            assume u in Y;

            then

            reconsider u9 = u as bag of n by A1;

            u9 <= (u9,T) by TERMORD: 6;

            then [u9, u9] in T by TERMORD:def 2;

            hence u in ( field T) by RELAT_1: 15;

          end;

          then Y c= ( field T) by TARSKI:def 3;

          hence ex a be object st a in Y & (T -Seg a) misses Y by A2, WELLORD1:def 2;

        end;

        then T is_well_founded_in the carrier of R by WELLORD1:def 3;

        hence thesis by WELLFND1:def 2;

      end;

    end

    

     Lm11: for n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L holds ( Support p) in ( Fin the carrier of RelStr (# ( Bags n), T #))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L;

      set sp = ( Support p);

      sp is finite by POLYNOM1:def 5;

      hence thesis by FINSUB_1:def 5;

    end;

    definition

      let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n, L;

      :: POLYRED:def2

      pred p <= q,T means [( Support p), ( Support q)] in ( FinOrd RelStr (# ( Bags n), T #));

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q be Polynomial of n, L;

      :: POLYRED:def3

      pred p < q,T means p <= (q,T) & ( Support p) <> ( Support q);

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L;

      :: POLYRED:def4

      func Support (p,T) -> Element of ( Fin the carrier of RelStr (# ( Bags n), T #)) equals ( Support p);

      coherence by Lm11;

    end

    theorem :: POLYRED:24

    

     Th24: for n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be non-zero Polynomial of n, L holds ( PosetMax ( Support (p,T))) = ( HT (p,T))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be non-zero Polynomial of n, L;

      set htp = ( HT (p,T)), R = RelStr (# ( Bags n), T #), sp = ( Support (p,T));

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

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

      then

       A1: htp in ( Support p) by TERMORD:def 6;

      now

        assume ex y be set st y in sp & y <> htp & [htp, y] in the InternalRel of R;

        then

        consider y be set such that

         A2: y in sp and

         A3: y <> htp and

         A4: [htp, y] in the InternalRel of R;

        y is Element of ( Bags n) by A2;

        then

        reconsider y9 = y as bag of n;

        y9 <= (htp,T) & htp <= (y9,T) by A2, A4, TERMORD:def 2, TERMORD:def 6;

        hence contradiction by A3, TERMORD: 7;

      end;

      then htp is_maximal_wrt (( Support (p,T)),the InternalRel of R) by A1, WAYBEL_4:def 23;

      hence thesis by A1, BAGORDER:def 13;

    end;

    theorem :: POLYRED:25

    

     Th25: for n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p be Polynomial of n, L holds p <= (p,T) by Lm11, ORDERS_1: 3;

    

     Lm12: for n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L holds ( 0_ (n,L)) <= (p,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L;

      set sp0 = ( Support ( 0_ (n,L))), sp = ( Support p), R = RelStr (# ( Bags n), T #);

      

       A1: sp is Element of ( Fin the carrier of R) by Lm11;

      sp0 = {} & sp0 is Element of ( Fin the carrier of R) by Lm11, POLYNOM7: 1;

      then [sp0, sp] in { [x, y] where x,y be Element of ( Fin the carrier of R) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R) } by A1;

      then

       A2: [sp0, sp] in (( FinOrd-Approx R) . 0 ) by BAGORDER:def 14;

      ( dom ( FinOrd-Approx R)) = NAT by BAGORDER:def 14;

      then (( FinOrd-Approx R) . 0 ) in ( rng ( FinOrd-Approx R)) by FUNCT_1: 3;

      then [sp0, sp] in ( union ( rng ( FinOrd-Approx R))) by A2, TARSKI:def 4;

      then [sp0, sp] in ( FinOrd R) by BAGORDER:def 15;

      hence thesis;

    end;

    theorem :: POLYRED:26

    

     Th26: for n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q be Polynomial of n, L holds p <= (q,T) & q <= (p,T) iff ( Support p) = ( Support q)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q be Polynomial of n, L;

      set O = ( FinOrd RelStr (# ( Bags n), T #));

       A1:

      now

        assume p <= (q,T) & q <= (p,T);

        then

         A2: [( Support p), ( Support q)] in O & [( Support q), ( Support p)] in O;

        ( Support p) in ( Fin the carrier of RelStr (# ( Bags n), T #)) & ( Support q) in ( Fin the carrier of RelStr (# ( Bags n), T #)) by Lm11;

        hence ( Support p) = ( Support q) by A2, ORDERS_1: 4;

      end;

      ( Support p) = ( Support q) implies p <= (q,T) & q <= (p,T) by Lm11, ORDERS_1: 3;

      hence thesis by A1;

    end;

    theorem :: POLYRED:27

    

     Th27: for n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q,r be Polynomial of n, L holds p <= (q,T) & q <= (r,T) implies p <= (r,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q,r be Polynomial of n, L;

      set O = ( FinOrd RelStr (# ( Bags n), T #));

      

       A1: ( Support r) in ( Fin the carrier of RelStr (# ( Bags n), T #)) by Lm11;

      assume p <= (q,T) & q <= (r,T);

      then

       A2: [( Support p), ( Support q)] in O & [( Support q), ( Support r)] in O;

      ( Support p) in ( Fin the carrier of RelStr (# ( Bags n), T #)) & ( Support q) in ( Fin the carrier of RelStr (# ( Bags n), T #)) by Lm11;

      then [( Support p), ( Support r)] in O by A2, A1, ORDERS_1: 5;

      hence thesis;

    end;

    theorem :: POLYRED:28

    

     Th28: for n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q be Polynomial of n, L holds p <= (q,T) or q <= (p,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q be Polynomial of n, L;

      set R = RelStr (# ( Bags n), T #), O = RelStr (# ( Fin the carrier of R), ( FinOrd R) #);

      reconsider sp = ( Support p), sq = ( Support q) as Element of O by Lm11;

      ( FinPoset R) is connected;

      then O is connected by BAGORDER:def 16;

      then sp <= sq or sq <= sp by WAYBEL_0:def 29;

      then [( Support p), ( Support q)] in ( FinOrd R) or [( Support q), ( Support p)] in ( FinOrd R) by ORDERS_2:def 5;

      hence thesis;

    end;

    theorem :: POLYRED:29

    

     Th29: for n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q be Polynomial of n, L holds p <= (q,T) iff not q < (p,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be non empty addLoopStr, p,q be Polynomial of n, L;

      

       A1: not q < (p,T) implies p <= (q,T)

      proof

        assume

         A2: not q < (p,T);

        now

          per cases by A2;

            case not ( Support q) <> ( Support p);

            hence thesis by Th26;

          end;

            case not q <= (p,T);

            hence thesis by Th28;

          end;

        end;

        hence thesis;

      end;

      p <= (q,T) implies not q < (p,T) by Th26;

      hence thesis by A1;

    end;

    

     Lm13: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L, b be bag of n holds [( HT (p,T)), b] in T & b <> ( HT (p,T)) implies (p . b) = ( 0. L)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L, b be bag of n;

      

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

      assume

       A2: [( HT (p,T)), b] in T & b <> ( HT (p,T));

      now

        assume b in ( Support p);

        then b <= (( HT (p,T)),T) by TERMORD:def 6;

        then [b, ( HT (p,T))] in T by TERMORD:def 2;

        hence contradiction by A2, A1, ORDERS_1: 4;

      end;

      hence thesis by A1, POLYNOM1:def 4;

    end;

    

     Lm14: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L st ( HT (p,T)) = ( EmptyBag n) holds ( Red (p,T)) = ( 0_ (n,L))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L;

      set red = ( Red (p,T)), e = ( 0_ (n,L));

      assume

       A1: ( HT (p,T)) = ( EmptyBag n);

       A2:

      now

        let b be bag of n;

        

         A3: [( EmptyBag n), b] in T by BAGORDER:def 5;

        assume b <> ( EmptyBag n);

        hence (p . b) = ( 0. L) by A1, A3, Lm13;

      end;

       A4:

      now

        let b be object;

        assume b in ( dom red);

        then

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

        

         A5: (red . b9) = ((p - ( HM (p,T))) . b9) by TERMORD:def 9

        .= ((p + ( - ( HM (p,T)))) . b9) by POLYNOM1:def 7

        .= ((p . b9) + (( - ( HM (p,T))) . b9)) by POLYNOM1: 15

        .= ((p . b9) + ( - (( HM (p,T)) . b9))) by POLYNOM1: 17;

        now

          per cases ;

            case b9 = ( EmptyBag n);

            

            hence (red . b9) = ((p . ( HT (p,T))) + ( - (p . ( HT (p,T))))) by A1, A5, TERMORD: 18

            .= ( 0. L) by RLVECT_1: 5

            .= (e . b9) by POLYNOM1: 22;

          end;

            case

             A6: b9 <> ( EmptyBag n);

            

            hence (red . b9) = (( 0. L) + ( - (( HM (p,T)) . b9))) by A2, A5

            .= (( 0. L) + ( - ( 0. L))) by A1, A6, TERMORD: 19

            .= ( 0. L) by RLVECT_1: 5

            .= (e . b9) by POLYNOM1: 22;

          end;

        end;

        hence (red . b) = (e . b);

      end;

      ( dom red) = ( Bags n) by FUNCT_2:def 1

      .= ( dom e) by FUNCT_2:def 1;

      hence thesis by A4, FUNCT_1: 2;

    end;

    

     Lm15: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p,q be Polynomial of n, L holds p < (q,T) iff (p = ( 0_ (n,L)) & q <> ( 0_ (n,L)) or ( HT (p,T)) < (( HT (q,T)),T) or ( HT (p,T)) = ( HT (q,T)) & ( Red (p,T)) < (( Red (q,T)),T))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p,q be Polynomial of n, L;

      set R = RelStr (# ( Bags n), T #), sp = ( Support p), sq = ( Support q), x = ( Support (p,T)), y = ( Support (q,T));

       A1:

      now

        assume

         A2: p = ( 0_ (n,L)) & q <> ( 0_ (n,L)) or ( HT (p,T)) < (( HT (q,T)),T) or ( HT (p,T)) = ( HT (q,T)) & ( Red (p,T)) < (( Red (q,T)),T);

        now

          per cases by A2;

            case

             A3: p = ( 0_ (n,L)) & q <> ( 0_ (n,L));

            then ( Support p) = {} by POLYNOM7: 1;

            then

             A4: ( Support p) <> ( Support q) by A3, POLYNOM7: 1;

            p <= (q,T) by A3, Lm12;

            hence p < (q,T) by A4;

          end;

            case

             A5: ( HT (p,T)) < (( HT (q,T)),T);

            then

             A6: ( HT (p,T)) <> ( HT (q,T)) by TERMORD:def 3;

            

             A7: ( HT (p,T)) <= (( HT (q,T)),T) by A5, TERMORD:def 3;

            then

             A8: [( HT (p,T)), ( HT (q,T))] in T by TERMORD:def 2;

            now

              per cases ;

                case

                 A9: sp = {} ;

                then

                 A10: p = ( 0_ (n,L)) by POLYNOM7: 1;

                 A11:

                now

                  assume sp = sq;

                  then ( HT (p,T)) = ( HT (q,T)) by A9, A10, POLYNOM7: 1;

                  hence contradiction by A5, TERMORD:def 3;

                end;

                p <= (q,T) by A10, Lm12;

                hence p < (q,T) by A11;

              end;

                case

                 A12: sp <> {} ;

                 A13:

                now

                  assume sq = {} ;

                  then ( HT (q,T)) = ( EmptyBag n) by TERMORD:def 6;

                  then [( HT (q,T)), ( HT (p,T))] in T by BAGORDER:def 5;

                  then ( HT (q,T)) <= (( HT (p,T)),T) by TERMORD:def 2;

                  hence contradiction by A7, A6, TERMORD: 7;

                end;

                 A14:

                now

                  assume

                   A15: sp = sq;

                  ( HT (q,T)) in sq by A13, TERMORD:def 6;

                  then

                   A16: ( HT (q,T)) <= (( HT (p,T)),T) by A15, TERMORD:def 6;

                  ( HT (p,T)) in sp by A12, TERMORD:def 6;

                  then ( HT (p,T)) <= (( HT (q,T)),T) by A15, TERMORD:def 6;

                  hence contradiction by A6, A16, TERMORD: 7;

                end;

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

                then p is non-zero;

                then

                 A17: ( PosetMax ( Support (p,T))) = ( HT (p,T)) by Th24;

                q <> ( 0_ (n,L)) by A13, POLYNOM7: 1;

                then q is non-zero;

                then ( PosetMax ( Support (q,T))) = ( HT (q,T)) by Th24;

                then [x, y] in ( union ( rng ( FinOrd-Approx R))) by A6, A8, A12, A13, A17, BAGORDER: 35;

                then [sp, sq] in ( FinOrd R) by BAGORDER:def 15;

                then p <= (q,T);

                hence p < (q,T) by A14;

              end;

            end;

            hence p < (q,T);

          end;

            case

             A18: ( HT (p,T)) = ( HT (q,T)) & ( Red (p,T)) < (( Red (q,T)),T);

            then ( Red (p,T)) <= (( Red (q,T)),T);

            then

             A19: [( Support ( Red (p,T))), ( Support ( Red (q,T)))] in ( FinOrd R);

            now

              per cases ;

                case sp = {} ;

                then

                 A20: ( HT (p,T)) = ( EmptyBag n) by TERMORD:def 6;

                then ( Red (p,T)) = ( 0_ (n,L)) by Lm14;

                then ( Support ( Red (q,T))) = ( Support ( Red (p,T))) by A18, A20, Lm14;

                hence contradiction by A18;

              end;

                case

                 A21: sp <> {} ;

                now

                  per cases ;

                    case sq = {} ;

                    then

                     A22: ( HT (q,T)) = ( EmptyBag n) by TERMORD:def 6;

                    then ( Red (q,T)) = ( 0_ (n,L)) by Lm14;

                    then ( Support ( Red (p,T))) = ( Support ( Red (q,T))) by A18, A22, Lm14;

                    hence contradiction by A18;

                  end;

                    case

                     A23: sq <> {} ;

                     A24:

                    now

                      assume sp = sq;

                      

                      then ( Support ( Red (p,T))) = (sq \ {( HT (q,T))}) by A18, TERMORD: 36

                      .= ( Support ( Red (q,T))) by TERMORD: 36;

                      hence contradiction by A18;

                    end;

                    set rp = ( Red (p,T)), rq = ( Red (q,T));

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

                    then

                     A25: p is non-zero;

                    q <> ( 0_ (n,L)) by A23, POLYNOM7: 1;

                    then

                     A26: q is non-zero;

                    then

                     A27: ( PosetMax ( Support (q,T))) = ( HT (q,T)) by Th24;

                    

                     A28: ( Support rq) = (( Support q) \ {( HT (q,T))}) by TERMORD: 36

                    .= (y \ {( PosetMax y)}) by A26, Th24;

                    ( Support rp) = (( Support p) \ {( HT (p,T))}) by TERMORD: 36

                    .= (x \ {( PosetMax x)}) by A25, Th24;

                    then

                     A29: [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng ( FinOrd-Approx R))) by A19, A28, BAGORDER:def 15;

                    ( PosetMax ( Support (p,T))) = ( HT (p,T)) by A25, Th24;

                    then [x, y] in ( union ( rng ( FinOrd-Approx R))) by A18, A21, A23, A27, A29, BAGORDER: 35;

                    then [sp, sq] in ( FinOrd R) by BAGORDER:def 15;

                    then p <= (q,T);

                    hence p < (q,T) by A24;

                  end;

                end;

                hence p < (q,T);

              end;

            end;

            hence p < (q,T);

          end;

        end;

        hence p < (q,T);

      end;

      now

        assume

         A30: p < (q,T);

        then p <= (q,T);

        then [sp, sq] in ( FinOrd R);

        then

         A31: [sp, sq] in ( union ( rng ( FinOrd-Approx R))) by BAGORDER:def 15;

        

         A32: ( Support p) <> ( Support q) by A30;

        now

          per cases by A31, BAGORDER: 35;

            case x = {} ;

            hence p = ( 0_ (n,L)) & q <> ( 0_ (n,L)) by A32, POLYNOM7: 1;

          end;

            case

             A33: x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R;

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

            then q is non-zero;

            then

             A34: ( PosetMax ( Support (q,T))) = ( HT (q,T)) by Th24;

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

            then p is non-zero;

            then

             A35: ( PosetMax ( Support (p,T))) = ( HT (p,T)) by Th24;

            then ( HT (p,T)) <= (( HT (q,T)),T) by A33, A34, TERMORD:def 2;

            hence ( HT (p,T)) < (( HT (q,T)),T) by A33, A35, A34, TERMORD:def 3;

          end;

            case

             A36: x <> {} & y <> {} & ( PosetMax x) = ( PosetMax y) & [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng ( FinOrd-Approx R)));

            set rp = ( Red (p,T)), rq = ( Red (q,T));

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

            then

             A37: p is non-zero;

            then

             A38: ( PosetMax ( Support (p,T))) = ( HT (p,T)) by Th24;

            q <> ( 0_ (n,L)) by A36, POLYNOM7: 1;

            then

             A39: q is non-zero;

            then

             A40: ( PosetMax ( Support (q,T))) = ( HT (q,T)) by Th24;

             A41:

            now

              ( HT (q,T)) in sq by A36, TERMORD:def 6;

              then for u be object holds u in {( HT (q,T))} implies u in sq by TARSKI:def 1;

              then

               A42: {( HT (q,T))} c= sq by TARSKI:def 3;

              ( Support rq) = (sq \ {( HT (q,T))}) by TERMORD: 36;

              

              then

               A43: (( Support rq) \/ {( HT (q,T))}) = (sq \/ {( HT (q,T))}) by XBOOLE_1: 39

              .= sq by A42, XBOOLE_1: 12;

              ( HT (p,T)) in sp by A36, TERMORD:def 6;

              then for u be object holds u in {( HT (p,T))} implies u in sp by TARSKI:def 1;

              then

               A44: {( HT (p,T))} c= sp by TARSKI:def 3;

              ( Support rp) = (sp \ {( HT (p,T))}) by TERMORD: 36;

              

              then

               A45: (( Support rp) \/ {( HT (p,T))}) = (sp \/ {( HT (p,T))}) by XBOOLE_1: 39

              .= sp by A44, XBOOLE_1: 12;

              assume ( Support ( Red (p,T))) = ( Support ( Red (q,T)));

              hence contradiction by A30, A36, A38, A40, A45, A43;

            end;

            

             A46: ( Support (rp,T)) = (( Support p) \ {( HT (p,T))}) by TERMORD: 36

            .= (x \ {( PosetMax x)}) by A37, Th24;

            ( Support (rq,T)) = (( Support q) \ {( HT (q,T))}) by TERMORD: 36

            .= (y \ {( PosetMax y)}) by A39, Th24;

            then [( Support (rp,T)), ( Support (rq,T))] in ( FinOrd R) by A36, A46, BAGORDER:def 15;

            then ( Red (p,T)) <= (( Red (q,T)),T);

            hence ( HT (p,T)) = ( HT (q,T)) & ( Red (p,T)) < (( Red (q,T)),T) by A36, A39, A38, A41, Th24;

          end;

        end;

        hence p = ( 0_ (n,L)) & q <> ( 0_ (n,L)) or ( HT (p,T)) < (( HT (q,T)),T) or ( HT (p,T)) = ( HT (q,T)) & ( Red (p,T)) < (( Red (q,T)),T);

      end;

      hence thesis by A1;

    end;

    theorem :: POLYRED:30

    for n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p be Polynomial of n, L holds ( 0_ (n,L)) <= (p,T) by Lm12;

    

     Lm16: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p,q be Polynomial of n, L st q <> ( 0_ (n,L)) holds ( HT (p,T)) = ( HT (q,T)) & ( Red (p,T)) <= (( Red (q,T)),T) implies p <= (q,T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p,q be Polynomial of n, L;

      assume

       A1: q <> ( 0_ (n,L));

      set x = ( Support (p,T)), y = ( Support (q,T));

      set rp = ( Red (p,T)), rq = ( Red (q,T));

      set R = RelStr (# ( Bags n), T #);

      assume that

       A2: ( HT (p,T)) = ( HT (q,T)) and

       A3: ( Red (p,T)) <= (( Red (q,T)),T);

       [( Support ( Red (p,T))), ( Support ( Red (q,T)))] in ( FinOrd R) by A3;

      then

       A4: [( Support ( Red (p,T))), ( Support ( Red (q,T)))] in ( union ( rng ( FinOrd-Approx R))) by BAGORDER:def 15;

      now

        per cases ;

          case p = ( 0_ (n,L));

          hence thesis by Lm12;

        end;

          case

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

          then

           A6: x <> {} by POLYNOM7: 1;

          

           A7: q is non-zero by A1;

          

           A8: p is non-zero by A5;

          

           A9: ( Support rp) = (( Support p) \ {( HT (p,T))}) by TERMORD: 36

          .= (x \ {( PosetMax x)}) by A8, Th24;

          

           A10: y <> {} by A1, POLYNOM7: 1;

          

           A11: ( Support rq) = (( Support q) \ {( HT (q,T))}) by TERMORD: 36

          .= (y \ {( PosetMax y)}) by A7, Th24;

          ( PosetMax x) = ( HT (q,T)) by A2, A8, Th24

          .= ( PosetMax y) by A7, Th24;

          then [x, y] in ( union ( rng ( FinOrd-Approx R))) by A4, A6, A10, A9, A11, BAGORDER: 35;

          then [x, y] in ( FinOrd R) by BAGORDER:def 15;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYRED:31

    

     Th31: for n be Nat, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive non trivial doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L)) holds ex p be Polynomial of n, L st p in P & for q be Polynomial of n, L st q in P holds p <= (q,T)

    proof

      let n be Nat, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive non trivial doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L));

      set P9 = { ( Support (p,T)) where p be Polynomial of n, L : p in P };

      set p = the Element of P;

      reconsider p as Polynomial of n, L by POLYNOM1:def 11;

      ( Support (p,T)) in P9;

      then

      reconsider P9 as non empty set;

      set R = RelStr (# ( Bags n), T #), FR = ( FinPoset R);

      set m = ( MinElement (P9,FR));

      

       A1: FR = RelStr (# ( Fin the carrier of R), ( FinOrd R) #) by BAGORDER:def 16;

      now

        let u be object;

        assume u in P9;

        then ex p be Polynomial of n, L st u = ( Support (p,T)) & p in P;

        hence u in the carrier of FR by A1;

      end;

      then

       A2: P9 c= the carrier of FR by TARSKI:def 3;

      

       A3: FR is well_founded by BAGORDER: 41;

      then m in P9 by A2, BAGORDER:def 17;

      then

      consider p be Polynomial of n, L such that

       A4: ( Support (p,T)) = m and

       A5: p in P;

      take p;

      

       A6: m is_minimal_wrt (P9,the InternalRel of FR) by A2, A3, BAGORDER:def 17;

      now

        let q be Polynomial of n, L;

        set sq = ( Support (q,T));

        assume q in P;

        then

         A7: sq in P9;

        now

          per cases ;

            case ( Support p) = ( Support q);

            hence p <= (q,T) by Th26;

          end;

            case ( Support p) <> ( Support q);

            then not [( Support (q,T)), m] in the InternalRel of FR by A6, A4, A7, WAYBEL_4:def 25;

            then not q <= (p,T) by A1, A4;

            hence p <= (q,T) by Th28;

          end;

        end;

        hence p <= (q,T);

      end;

      hence thesis by A5;

    end;

    theorem :: POLYRED:32

    for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p,q be Polynomial of n, L holds p < (q,T) iff (p = ( 0_ (n,L)) & q <> ( 0_ (n,L)) or ( HT (p,T)) < (( HT (q,T)),T) or ( HT (p,T)) = ( HT (q,T)) & ( Red (p,T)) < (( Red (q,T)),T)) by Lm15;

    theorem :: POLYRED:33

    

     Th33: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be non-zero Polynomial of n, L holds ( Red (p,T)) < (( HM (p,T)),T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be non-zero Polynomial of n, L;

      set red = ( Red (p,T)), htp = ( HT (p,T));

      set sred = ( Support red), sp = ( Support ( HM (p,T))), R = RelStr (# ( Bags n), T #);

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

      then

       A1: ( Support p) <> {} by POLYNOM7: 1;

      per cases ;

        suppose red = ( 0_ (n,L));

        then

         A2: sred = {} by POLYNOM7: 1;

        htp in ( Support p) by A1, TERMORD:def 6;

        then (p . htp) <> ( 0. L) by POLYNOM1:def 4;

        then (( HM (p,T)) . htp) <> ( 0. L) by TERMORD: 18;

        then

         A3: htp in ( Support ( HM (p,T))) by POLYNOM1:def 4;

        ( dom ( FinOrd-Approx R)) = NAT by BAGORDER:def 14;

        then

         A4: (( FinOrd-Approx R) . 0 ) in ( rng ( FinOrd-Approx R)) by FUNCT_1: 3;

        sred is Element of ( Fin the carrier of R) & sp is Element of ( Fin the carrier of R) by Lm11;

        then [sred, sp] in { [x, y] where x,y be Element of ( Fin the carrier of R) : x = {} or (x <> {} & y <> {} & ( PosetMax x) <> ( PosetMax y) & [( PosetMax x), ( PosetMax y)] in the InternalRel of R) } by A2;

        then [sred, sp] in (( FinOrd-Approx R) . 0 ) by BAGORDER:def 14;

        then [sred, sp] in ( union ( rng ( FinOrd-Approx R))) by A4, TARSKI:def 4;

        then [sred, sp] in ( FinOrd R) by BAGORDER:def 15;

        then red <= (( HM (p,T)),T);

        hence thesis by A2, A3;

      end;

        suppose red <> ( 0_ (n,L));

        then ( Support red) <> {} by POLYNOM7: 1;

        then

         A5: ( HT (red,T)) in ( Support red) by TERMORD:def 6;

         A6:

        now

          assume ( HT (red,T)) = htp;

          then (red . ( HT (red,T))) = ( 0. L) by TERMORD: 39;

          hence contradiction by A5, POLYNOM1:def 4;

        end;

        ( Support red) c= ( Support p) by TERMORD: 35;

        then ( HT (red,T)) <= (htp,T) by A5, TERMORD:def 6;

        then ( HT (red,T)) < (htp,T) by A6, TERMORD:def 3;

        then ( HT (red,T)) < (( HT (( HM (p,T)),T)),T) by TERMORD: 26;

        hence thesis by Lm15;

      end;

    end;

    theorem :: POLYRED:34

    

     Th34: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds ( HM (p,T)) <= (p,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p9 be Polynomial of n, L;

      per cases ;

        suppose

         A1: p9 = ( 0_ (n,L));

        now

          assume ( Support ( HM (p9,T))) <> {} ;

          then

          consider u be bag of n such that

           A2: ( Support ( HM (p9,T))) = {u} by POLYNOM7: 6;

          

           A3: u in ( Support ( HM (p9,T))) by A2, TARSKI:def 1;

          now

            let v be bag of n;

            assume v in ( Support ( HM (p9,T)));

            then u = v by A2, TARSKI:def 1;

            hence v <= (u,T) by TERMORD: 6;

          end;

          then

           A4: ( HT (( HM (p9,T)),T)) = u by A3, TERMORD:def 6;

          ( 0. L) = (p9 . ( HT (p9,T))) by A1, POLYNOM1: 22

          .= ( HC (p9,T)) by TERMORD:def 7

          .= ( HC (( HM (p9,T)),T)) by TERMORD: 27

          .= (( HM (p9,T)) . u) by A4, TERMORD:def 7;

          hence contradiction by A3, POLYNOM1:def 4;

        end;

        then ( HM (p9,T)) = ( 0_ (n,L)) by POLYNOM7: 1;

        hence thesis by A1, Th25;

      end;

        suppose p9 <> ( 0_ (n,L));

        then

        reconsider p = p9 as non-zero Polynomial of n, L by POLYNOM7:def 1;

        set hmp = ( HM (p,T)), R = RelStr (# ( Bags n), T #);

        set x = ( Support (hmp,T)), y = ( Support (p,T));

        

         A5: (x \ {( PosetMax x)}) is Element of ( Fin the carrier of R) & (y \ {( PosetMax y)}) is Element of ( Fin the carrier of R) by BAGORDER: 37;

        

         A6: ( PosetMax x) = ( HT (hmp,T)) by Th24

        .= ( HT (p,T)) by TERMORD: 26;

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

        then

         A7: ( Support p) <> {} by POLYNOM7: 1;

        (hmp . ( HT (p,T))) = (p . ( HT (p,T))) by TERMORD: 18

        .= ( HC (p,T)) by TERMORD:def 7;

        then

         A8: (hmp . ( HT (p,T))) <> ( 0. L);

        then

         A9: x <> {} by POLYNOM1:def 4;

        ( HT (p,T)) in ( Support hmp) by A8, POLYNOM1:def 4;

        then ( Support hmp) = {( HT (p,T))} by TERMORD: 21;

        then (x \ {( PosetMax x)}) = {} by A6, XBOOLE_1: 37;

        then

         A10: [(x \ {( PosetMax x)}), (y \ {( PosetMax y)})] in ( union ( rng ( FinOrd-Approx R))) by A5, BAGORDER: 35;

        ( PosetMax x) = ( PosetMax y) by A6, Th24;

        then [x, y] in ( union ( rng ( FinOrd-Approx R))) by A7, A9, A10, BAGORDER: 35;

        then [x, y] in ( FinOrd R) by BAGORDER:def 15;

        hence thesis;

      end;

    end;

    theorem :: POLYRED:35

    

     Th35: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be non-zero Polynomial of n, L holds ( Red (p,T)) < (p,T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be non-zero Polynomial of n, L;

      (( Red (p,T)) . ( HT (p,T))) = ( 0. L) by TERMORD: 39;

      then

       A1: not ( HT (p,T)) in ( Support ( Red (p,T))) by POLYNOM1:def 4;

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

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

      then

       A2: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

      ( Red (p,T)) < (( HM (p,T)),T) by Th33;

      then

       A3: ( Red (p,T)) <= (( HM (p,T)),T);

      ( HM (p,T)) <= (p,T) by Th34;

      then ( Red (p,T)) <= (p,T) by A3, Th27;

      hence thesis by A2, A1;

    end;

    begin

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L, b be bag of n;

      :: POLYRED:def5

      pred f reduces_to g,p,b,T means f <> ( 0_ (n,L)) & p <> ( 0_ (n,L)) & b in ( Support f) & ex s be bag of n st (s + ( HT (p,T))) = b & g = (f - (((f . b) / ( HC (p,T))) * (s *' p)));

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L;

      :: POLYRED:def6

      pred f reduces_to g,p,T means ex b be bag of n st f reduces_to (g,p,b,T);

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L));

      :: POLYRED:def7

      pred f reduces_to g,P,T means ex p be Polynomial of n, L st p in P & f reduces_to (g,p,T);

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n, L;

      :: POLYRED:def8

      pred f is_reducible_wrt p,T means ex g be Polynomial of n, L st f reduces_to (g,p,T);

    end

    notation

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n, L;

      antonym f is_irreducible_wrt p,T for f is_reducible_wrt p,T;

      antonym f is_in_normalform_wrt p,T for f is_reducible_wrt p,T;

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L));

      :: POLYRED:def9

      pred f is_reducible_wrt P,T means ex g be Polynomial of n, L st f reduces_to (g,P,T);

    end

    notation

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L));

      antonym f is_irreducible_wrt P,T for f is_reducible_wrt P,T;

      antonym f is_in_normalform_wrt P,T for f is_reducible_wrt P,T;

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L;

      :: POLYRED:def10

      pred f top_reduces_to g,p,T means f reduces_to (g,p,( HT (f,T)),T);

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p be Polynomial of n, L;

      :: POLYRED:def11

      pred f is_top_reducible_wrt p,T means ex g be Polynomial of n, L st f top_reduces_to (g,p,T);

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L));

      :: POLYRED:def12

      pred f is_top_reducible_wrt P,T means ex p be Polynomial of n, L st p in P & f is_top_reducible_wrt (p,T);

    end

    theorem :: POLYRED:36

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, p be non-zero Polynomial of n, L holds f is_reducible_wrt (p,T) iff ex b be bag of n st b in ( Support f) & ( HT (p,T)) divides b

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, p be non-zero Polynomial of n, L;

       A1:

      now

        

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

        assume ex b be bag of n st b in ( Support f) & ( HT (p,T)) divides b;

        then

        consider b be bag of n such that

         A3: b in ( Support f) and

         A4: ( HT (p,T)) divides b;

        consider s be bag of n such that

         A5: b = (( HT (p,T)) + s) by A4, TERMORD: 1;

        set g = (f - (((f . b) / ( HC (p,T))) * (s *' p)));

        f <> ( 0_ (n,L)) by A3, POLYNOM7: 1;

        then f reduces_to (g,p,b,T) by A3, A5, A2;

        then f reduces_to (g,p,T);

        hence f is_reducible_wrt (p,T);

      end;

      now

        assume f is_reducible_wrt (p,T);

        then

        consider g be Polynomial of n, L such that

         A6: f reduces_to (g,p,T);

        consider b be bag of n such that

         A7: f reduces_to (g,p,b,T) by A6;

        ex s be bag of n st (s + ( HT (p,T))) = b & g = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A7;

        then

         A8: ( HT (p,T)) divides b by TERMORD: 1;

        b in ( Support f) by A7;

        hence ex b be bag of n st b in ( Support f) & ( HT (p,T)) divides b by A8;

      end;

      hence thesis by A1;

    end;

    

     Lm17: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L, b be bag of n holds f reduces_to (g,p,b,T) implies not (b in ( Support g))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L, b be bag of n;

      assume

       A1: f reduces_to (g,p,b,T);

      then b in ( Support f) & ex s be bag of n st (s + ( HT (p,T))) = b & g = (f - (((f . b) / ( HC (p,T))) * (s *' p)));

      then

      consider s be bag of n such that b in ( Support f) and

       A2: (s + ( HT (p,T))) = b and

       A3: g = (f - (((f . b) / ( HC (p,T))) * (s *' p)));

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

      then

       A4: ( HC (p,T)) <> ( 0. L) by TERMORD: 17;

      set q = (((f . b) / ( HC (p,T))) * (s *' p));

      

       A5: (q . b) = (((f . b) / ( HC (p,T))) * ((s *' p) . b)) by POLYNOM7:def 9

      .= (((f . b) / ( HC (p,T))) * (p . ( HT (p,T)))) by A2, Lm9

      .= (((f . b) / ( HC (p,T))) * ( HC (p,T))) by TERMORD:def 7

      .= (((f . b) * (( HC (p,T)) " )) * ( HC (p,T)))

      .= ((f . b) * ((( HC (p,T)) " ) * ( HC (p,T)))) by GROUP_1:def 3

      .= ((f . b) * ( 1. L)) by A4, VECTSP_1:def 10

      .= (f . b);

      g = (f + ( - q)) by A3, POLYNOM1:def 7;

      

      then (g . b) = ((f . b) + (( - q) . b)) by POLYNOM1: 15

      .= ((f . b) + ( - (q . b))) by POLYNOM1: 17

      .= ( 0. L) by A5, RLVECT_1: 5;

      hence thesis by POLYNOM1:def 4;

    end;

    theorem :: POLYRED:37

    

     Th37: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p be Polynomial of n, L holds ( 0_ (n,L)) is_irreducible_wrt (p,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p be Polynomial of n, L;

      assume ( 0_ (n,L)) is_reducible_wrt (p,T);

      then

      consider g be Polynomial of n, L such that

       A1: ( 0_ (n,L)) reduces_to (g,p,T);

      ex b be bag of n st ( 0_ (n,L)) reduces_to (g,p,b,T) by A1;

      hence thesis;

    end;

    theorem :: POLYRED:38

    for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,p be Polynomial of n, L, m be non-zero Monomial of n, L holds f reduces_to ((f - (m *' p)),p,T) implies ( HT ((m *' p),T)) in ( Support f)

    proof

      let n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,p be Polynomial of n, L, m be non-zero Monomial of n, L;

      assume f reduces_to ((f - (m *' p)),p,T);

      then

      consider b be bag of n such that

       A1: f reduces_to ((f - (m *' p)),p,b,T);

      

       A2: p <> ( 0_ (n,L)) by A1;

      then

       A3: p is non-zero;

      

       A4: ( HC (p,T)) <> ( 0. L) by A2, TERMORD: 17;

       A5:

      now

        assume (( HC (p,T)) " ) = ( 0. L);

        

        then ( 0. L) = (( HC (p,T)) * (( HC (p,T)) " ))

        .= ( 1. L) by A4, VECTSP_1:def 10;

        hence contradiction;

      end;

      b in ( Support f) by A1;

      then (f . b) <> ( 0. L) by POLYNOM1:def 4;

      then ((f . b) * (( HC (p,T)) " )) <> ( 0. L) by A5, VECTSP_2:def 1;

      then ((f . b) / ( HC (p,T))) <> ( 0. L);

      then

       A6: ((f . b) / ( HC (p,T))) is non zero;

      consider s be bag of n such that

       A7: (s + ( HT (p,T))) = b and

       A8: (f - (m *' p)) = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A1;

      

       A9: (((f . b) / ( HC (p,T))) * (s *' p)) = ( - ( - (((f . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1: 19;

      f = (f + ( 0_ (n,L))) by POLYNOM1: 23

      .= (f + ((m *' p) - (m *' p))) by POLYNOM1: 24

      .= (f + ((m *' p) + ( - (m *' p)))) by POLYNOM1:def 7

      .= ((f + ( - (m *' p))) + (m *' p)) by POLYNOM1: 21

      .= ((m *' p) + (f - (((f . b) / ( HC (p,T))) * (s *' p)))) by A8, POLYNOM1:def 7;

      

      then ( 0_ (n,L)) = (f - ((m *' p) + (f - (((f . b) / ( HC (p,T))) * (s *' p))))) by POLYNOM1: 24

      .= (f + ( - ((m *' p) + (f - (((f . b) / ( HC (p,T))) * (s *' p)))))) by POLYNOM1:def 7

      .= (f + (( - (m *' p)) + ( - (f - (((f . b) / ( HC (p,T))) * (s *' p)))))) by Th1

      .= (f + (( - (m *' p)) + ( - (f + ( - (((f . b) / ( HC (p,T))) * (s *' p))))))) by POLYNOM1:def 7

      .= (f + (( - (m *' p)) + (( - f) + ( - ( - (((f . b) / ( HC (p,T))) * (s *' p))))))) by Th1

      .= (f + (( - f) + (( - (m *' p)) + (((f . b) / ( HC (p,T))) * (s *' p))))) by A9, POLYNOM1: 21

      .= ((f + ( - f)) + (( - (m *' p)) + (((f . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1: 21

      .= ((f - f) + (( - (m *' p)) + (((f . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1:def 7

      .= (( 0_ (n,L)) + (( - (m *' p)) + (((f . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1: 24

      .= (( - (m *' p)) + (((f . b) / ( HC (p,T))) * (s *' p))) by Th2;

      

      then (m *' p) = ((m *' p) + (( - (m *' p)) + (((f . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1: 23

      .= (((m *' p) + ( - (m *' p))) + (((f . b) / ( HC (p,T))) * (s *' p))) by POLYNOM1: 21

      .= (((m *' p) - (m *' p)) + (((f . b) / ( HC (p,T))) * (s *' p))) by POLYNOM1:def 7

      .= (( 0_ (n,L)) + (((f . b) / ( HC (p,T))) * (s *' p))) by POLYNOM1: 24

      .= (((f . b) / ( HC (p,T))) * (s *' p)) by Th2;

      

      then ( HT ((m *' p),T)) = ( HT ((s *' p),T)) by A6, Th21

      .= b by A7, A3, Th15;

      hence thesis by A1;

    end;

    theorem :: POLYRED:39

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n, L, b be bag of n holds f reduces_to (g,p,b,T) implies not (b in ( Support g)) by Lm17;

    theorem :: POLYRED:40

    

     Th40: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L, b,b9 be bag of n st b < (b9,T) holds f reduces_to (g,p,b,T) implies (b9 in ( Support g) iff b9 in ( Support f))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L, b,b9 be bag of n;

      assume

       A1: b < (b9,T);

      assume f reduces_to (g,p,b,T);

      then

      consider s be bag of n such that

       A2: (s + ( HT (p,T))) = b and

       A3: g = (f - (((f . b) / ( HC (p,T))) * (s *' p)));

      

       A4: b9 is Element of ( Bags n) by PRE_POLY:def 12;

       A5:

      now

        assume b9 in ( Support (s *' p));

        then

         A6: b9 <= (b,T) by A2, Th16;

        b <= (b9,T) by A1, TERMORD:def 3;

        then b = b9 by A6, TERMORD: 7;

        hence contradiction by A1, TERMORD:def 3;

      end;

       A7:

      now

        

         A8: ((((f . b) / ( HC (p,T))) * (s *' p)) . b9) = (((f . b) / ( HC (p,T))) * ((s *' p) . b9)) by POLYNOM7:def 9

        .= (((f . b) / ( HC (p,T))) * ( 0. L)) by A4, A5, POLYNOM1:def 4

        .= ( 0. L);

        assume

         A9: b9 in ( Support f);

        ((f - (((f . b) / ( HC (p,T))) * (s *' p))) . b9) = ((f + ( - (((f . b) / ( HC (p,T))) * (s *' p)))) . b9) by POLYNOM1:def 7

        .= ((f . b9) + (( - (((f . b) / ( HC (p,T))) * (s *' p))) . b9)) by POLYNOM1: 15

        .= ((f . b9) + ( - ( 0. L))) by A8, POLYNOM1: 17

        .= ((f . b9) + ( 0. L)) by RLVECT_1: 12

        .= (f . b9) by RLVECT_1:def 4;

        then (g . b9) <> ( 0. L) by A3, A9, POLYNOM1:def 4;

        hence b9 in ( Support g) by A4, POLYNOM1:def 4;

      end;

      now

        

         A10: ((((f . b) / ( HC (p,T))) * (s *' p)) . b9) = (((f . b) / ( HC (p,T))) * ((s *' p) . b9)) by POLYNOM7:def 9

        .= (((f . b) / ( HC (p,T))) * ( 0. L)) by A4, A5, POLYNOM1:def 4

        .= ( 0. L);

        assume

         A11: b9 in ( Support g);

        ((f - (((f . b) / ( HC (p,T))) * (s *' p))) . b9) = ((f + ( - (((f . b) / ( HC (p,T))) * (s *' p)))) . b9) by POLYNOM1:def 7

        .= ((f . b9) + (( - (((f . b) / ( HC (p,T))) * (s *' p))) . b9)) by POLYNOM1: 15

        .= ((f . b9) + ( - ( 0. L))) by A10, POLYNOM1: 17

        .= ((f . b9) + ( 0. L)) by RLVECT_1: 12

        .= (f . b9) by RLVECT_1:def 4;

        then (f . b9) <> ( 0. L) by A3, A11, POLYNOM1:def 4;

        hence b9 in ( Support f) by A4, POLYNOM1:def 4;

      end;

      hence thesis by A7;

    end;

    theorem :: POLYRED:41

    

     Th41: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L, b,b9 be bag of n st b < (b9,T) holds f reduces_to (g,p,b,T) implies (f . b9) = (g . b9)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,p,g be Polynomial of n, L, b,b9 be bag of n;

      assume

       A1: b < (b9,T);

      assume f reduces_to (g,p,b,T);

      then

      consider s be bag of n such that

       A2: (s + ( HT (p,T))) = b and

       A3: g = (f - (((f . b) / ( HC (p,T))) * (s *' p)));

       A4:

      now

        assume b9 in ( Support (s *' p));

        then

         A5: b9 <= (b,T) by A2, Th16;

        b <= (b9,T) by A1, TERMORD:def 3;

        then b = b9 by A5, TERMORD: 7;

        hence contradiction by A1, TERMORD:def 3;

      end;

      

       A6: b9 is Element of ( Bags n) by PRE_POLY:def 12;

      

       A7: ((((f . b) / ( HC (p,T))) * (s *' p)) . b9) = (((f . b) / ( HC (p,T))) * ((s *' p) . b9)) by POLYNOM7:def 9

      .= (((f . b) / ( HC (p,T))) * ( 0. L)) by A6, A4, POLYNOM1:def 4

      .= ( 0. L);

      ((f - (((f . b) / ( HC (p,T))) * (s *' p))) . b9) = ((f + ( - (((f . b) / ( HC (p,T))) * (s *' p)))) . b9) by POLYNOM1:def 7

      .= ((f . b9) + (( - (((f . b) / ( HC (p,T))) * (s *' p))) . b9)) by POLYNOM1: 15

      .= ((f . b9) + ( - ( 0. L))) by A7, POLYNOM1: 17

      .= ((f . b9) + ( 0. L)) by RLVECT_1: 12

      .= (f . b9) by RLVECT_1:def 4;

      hence thesis by A3;

    end;

    theorem :: POLYRED:42

    

     Th42: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n, L holds f reduces_to (g,p,T) implies for b be bag of n st b in ( Support g) holds b <= (( HT (f,T)),T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n, L;

      

       A1: T is_connected_in ( field T) by RELAT_2:def 14;

      assume f reduces_to (g,p,T);

      then

      consider b be bag of n such that

       A2: f reduces_to (g,p,b,T);

      b in ( Support f) by A2;

      then

       A3: b <= (( HT (f,T)),T) by TERMORD:def 6;

      now

        let u be bag of n;

        assume

         A4: u in ( Support g);

        now

          per cases ;

            case u = b;

            hence contradiction by A2, A4, Lm17;

          end;

            case

             A5: u <> b;

            b <= (b,T) by TERMORD: 6;

            then [b, b] in T by TERMORD:def 2;

            then

             A6: b in ( field T) by RELAT_1: 15;

            u <= (u,T) by TERMORD: 6;

            then [u, u] in T by TERMORD:def 2;

            then u in ( field T) by RELAT_1: 15;

            then

             A7: [u, b] in T or [b, u] in T by A1, A5, A6, RELAT_2:def 6;

            now

              per cases by A7, TERMORD:def 2;

                case u <= (b,T);

                hence u <= (( HT (f,T)),T) by A3, TERMORD: 8;

              end;

                case b <= (u,T);

                then b < (u,T) by A5, TERMORD:def 3;

                then u in ( Support f) iff u in ( Support g) by A2, Th40;

                hence u <= (( HT (f,T)),T) by A4, TERMORD:def 6;

              end;

            end;

            hence u <= (( HT (f,T)),T);

          end;

        end;

        hence u <= (( HT (f,T)),T);

      end;

      hence thesis;

    end;

    theorem :: POLYRED:43

    

     Th43: for n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n, L holds f reduces_to (g,p,T) implies g < (f,T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,p,g be Polynomial of n, L;

      set R = RelStr (# ( Bags n), T #);

      defpred P[ Nat] means for f,p,g be Polynomial of n, L holds ( card ( Support f)) = $1 & f reduces_to (g,p,T) implies [( Support g), ( Support f)] in ( FinOrd R);

      

       A1: ex k be Nat st ( card ( Support f)) = k;

      assume

       A2: f reduces_to (g,p,T);

      then

      consider b be bag of n such that

       A3: f reduces_to (g,p,b,T);

      

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

      proof

        let k be Nat;

        assume

         A5: for f,p,g be Polynomial of n, L holds ( card ( Support f)) = k & f reduces_to (g,p,T) implies [( Support g), ( Support f)] in ( FinOrd R);

        now

          

           A6: T is_connected_in ( field T) by RELAT_2:def 14;

          let f,p,g be Polynomial of n, L;

          assume that

           A7: ( card ( Support f)) = (k + 1) and

           A8: f reduces_to (g,p,T);

          consider b be bag of n such that

           A9: f reduces_to (g,p,b,T) by A8;

          consider s be bag of n such that

           A10: (s + ( HT (p,T))) = b and

           A11: g = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A9;

          

           A12: b in ( Support f) by A9;

          

           A13: f <> ( 0_ (n,L)) by A9;

          now

            per cases ;

              case

               A14: ( HT (f,T)) <> ( HT (g,T));

              ( HT (g,T)) <= (( HT (g,T)),T) by TERMORD: 6;

              then [( HT (g,T)), ( HT (g,T))] in T by TERMORD:def 2;

              then

               A15: ( HT (g,T)) in ( field T) by RELAT_1: 15;

              ( HT (f,T)) <= (( HT (f,T)),T) by TERMORD: 6;

              then [( HT (f,T)), ( HT (f,T))] in T by TERMORD:def 2;

              then ( HT (f,T)) in ( field T) by RELAT_1: 15;

              then

               A16: [( HT (f,T)), ( HT (g,T))] in T or [( HT (g,T)), ( HT (f,T))] in T by A6, A14, A15, RELAT_2:def 6;

              now

                per cases by A16, TERMORD:def 2;

                  case

                   A17: ( HT (f,T)) <= (( HT (g,T)),T);

                  now

                    assume not ( HT (g,T)) in ( Support g);

                    then ( HT (g,T)) = ( EmptyBag n) by TERMORD:def 6;

                    then [( HT (g,T)), ( HT (f,T))] in T by BAGORDER:def 5;

                    then ( HT (g,T)) <= (( HT (f,T)),T) by TERMORD:def 2;

                    hence contradiction by A14, A17, TERMORD: 7;

                  end;

                  then ( HT (g,T)) <= (( HT (f,T)),T) by A8, Th42;

                  hence [( Support g), ( Support f)] in ( FinOrd R) by A14, A17, TERMORD: 7;

                end;

                  case ( HT (g,T)) <= (( HT (f,T)),T);

                  then ( HT (g,T)) < (( HT (f,T)),T) by A14, TERMORD:def 3;

                  then g < (f,T) by Lm15;

                  then g <= (f,T);

                  hence [( Support g), ( Support f)] in ( FinOrd R);

                end;

              end;

              hence [( Support g), ( Support f)] in ( FinOrd R);

            end;

              case

               A18: ( HT (g,T)) = ( HT (f,T));

              now

                per cases ;

                  case b = ( HT (f,T));

                  then not ( HT (g,T)) in ( Support g) by A9, A18, Lm17;

                  then ( Support g) = {} by TERMORD:def 6;

                  then g = ( 0_ (n,L)) by POLYNOM7: 1;

                  then g <= (f,T) by Lm12;

                  hence [( Support g), ( Support f)] in ( FinOrd R);

                end;

                  case

                   A19: b <> ( HT (f,T));

                  ( HT (f,T)) in ( Support f) by A12, TERMORD:def 6;

                  then for u be object holds u in {( HT (f,T))} implies u in ( Support f) by TARSKI:def 1;

                  then

                   A20: {( HT (f,T))} c= ( Support f) by TARSKI:def 3;

                  

                   A21: ( Support ( Red (f,T))) = (( Support f) \ {( HT (f,T))}) by TERMORD: 36;

                   not b in {( HT (f,T))} by A19, TARSKI:def 1;

                  then

                   A22: b in ( Support ( Red (f,T))) by A12, A21, XBOOLE_0:def 5;

                  then ( Red (f,T)) <> ( 0_ (n,L)) by POLYNOM7: 1;

                  then

                  reconsider rf = ( Red (f,T)) as non-zero Polynomial of n, L by POLYNOM7:def 1;

                  

                   A23: rf <> ( 0_ (n,L)) & p <> ( 0_ (n,L)) by A9, POLYNOM7:def 1;

                  b <= (( HT (f,T)),T) by A12, TERMORD:def 6;

                  then b < (( HT (f,T)),T) by A19, TERMORD:def 3;

                  then (f . ( HT (f,T))) = (g . ( HT (g,T))) by A9, A18, Th41;

                  

                  then ( HC (f,T)) = (g . ( HT (g,T))) by TERMORD:def 7

                  .= ( HC (g,T)) by TERMORD:def 7;

                  

                  then ( HM (f,T)) = ( Monom (( HC (g,T)),( HT (g,T)))) by A18, TERMORD:def 8

                  .= ( HM (g,T)) by TERMORD:def 8;

                  

                  then ( Red (g,T)) = ((f - (((f . b) / ( HC (p,T))) * (s *' p))) - ( HM (f,T))) by A11, TERMORD:def 9

                  .= (((( HM (f,T)) + rf) - (((f . b) / ( HC (p,T))) * (s *' p))) - ( HM (f,T))) by TERMORD: 38

                  .= (((( HM (f,T)) + rf) - (((rf . b) / ( HC (p,T))) * (s *' p))) - ( HM (f,T))) by A12, A19, TERMORD: 40

                  .= (((( HM (f,T)) + rf) + ( - (((rf . b) / ( HC (p,T))) * (s *' p)))) - ( HM (f,T))) by POLYNOM1:def 7

                  .= ((( HM (f,T)) + (rf + ( - (((rf . b) / ( HC (p,T))) * (s *' p))))) - ( HM (f,T))) by POLYNOM1: 21

                  .= ((( HM (f,T)) + (rf + ( - (((rf . b) / ( HC (p,T))) * (s *' p))))) + ( - ( HM (f,T)))) by POLYNOM1:def 7

                  .= ((rf + ( - (((rf . b) / ( HC (p,T))) * (s *' p)))) + (( HM (f,T)) + ( - ( HM (f,T))))) by POLYNOM1: 21

                  .= ((rf - (((rf . b) / ( HC (p,T))) * (s *' p))) + (( HM (f,T)) + ( - ( HM (f,T))))) by POLYNOM1:def 7

                  .= ((rf - (((rf . b) / ( HC (p,T))) * (s *' p))) + (( HM (f,T)) - ( HM (f,T)))) by POLYNOM1:def 7

                  .= ((rf - (((rf . b) / ( HC (p,T))) * (s *' p))) + ( 0_ (n,L))) by POLYNOM1: 24

                  .= (rf - (((rf . b) / ( HC (p,T))) * (s *' p))) by POLYNOM1: 23;

                  then rf reduces_to (( Red (g,T)),p,b,T) by A10, A22, A23;

                  then

                   A24: rf reduces_to (( Red (g,T)),p,T);

                  ( HT (f,T)) in {( HT (f,T))} by TARSKI:def 1;

                  then

                   A25: not ( HT (f,T)) in ( Support ( Red (f,T))) by A21, XBOOLE_0:def 5;

                  (( Support ( Red (f,T))) \/ {( HT (f,T))}) = (( Support f) \/ {( HT (f,T))}) by A21, XBOOLE_1: 39

                  .= ( Support f) by A20, XBOOLE_1: 12;

                  then (( card ( Support ( Red (f,T)))) + 1) = (k + 1) by A7, A25, CARD_2: 41;

                  then [( Support ( Red (g,T))), ( Support rf)] in ( FinOrd R) by A5, A24, XCMPLX_1: 2;

                  then ( Red (g,T)) <= (( Red (f,T)),T);

                  then g <= (f,T) by A13, A18, Lm16;

                  hence [( Support g), ( Support f)] in ( FinOrd R);

                end;

              end;

              hence [( Support g), ( Support f)] in ( FinOrd R);

            end;

          end;

          hence [( Support g), ( Support f)] in ( FinOrd R);

        end;

        hence thesis;

      end;

      

       A26: P[ 0 ]

      proof

        let f,p,g be Polynomial of n, L;

        assume that

         A27: ( card ( Support f)) = 0 and

         A28: f reduces_to (g,p,T);

        ( Support f) = {} by A27;

        then f = ( 0_ (n,L)) by POLYNOM7: 1;

        then f is_irreducible_wrt (p,T) by Th37;

        hence thesis by A28;

      end;

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

      then [( Support g), ( Support f)] in ( FinOrd R) by A2, A1;

      then

       A29: g <= (f,T);

      ( Support f) <> ( Support g) by A3, Lm17;

      hence thesis by A29;

    end;

    begin

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      :: POLYRED:def13

      func PolyRedRel (P,T) -> Relation of ( NonZero ( Polynom-Ring (n,L))), the carrier of ( Polynom-Ring (n,L)) means

      : Def13: for p,q be Polynomial of n, L holds [p, q] in it iff p reduces_to (q,P,T);

      existence

      proof

        defpred P[ object, object] means ex p,q be Polynomial of n, L st p = $1 & q = $2 & p reduces_to (q,P,T);

        set A = ( NonZero ( Polynom-Ring (n,L))), B = the carrier of ( Polynom-Ring (n,L));

        consider R be Relation of A, B such that

         A1: for x,y be object holds [x, y] in R iff x in A & y in B & P[x, y] from RELSET_1:sch 1;

        take R;

        now

          let p,q be Polynomial of n, L;

           A2:

          now

            assume

             A3: p reduces_to (q,P,T);

            then

            consider pp be Polynomial of n, L such that pp in P and

             A4: p reduces_to (q,pp,T);

            ex b be bag of n st p reduces_to (q,pp,b,T) by A4;

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

            then

             A5: not p in {( 0_ (n,L))} by TARSKI:def 1;

            

             A6: q in B by POLYNOM1:def 11;

            ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) & p in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            then p in A by A5, XBOOLE_0:def 5;

            hence [p, q] in R by A1, A3, A6;

          end;

          now

            assume [p, q] in R;

            then P[p, q] by A1;

            hence p reduces_to (q,P,T);

          end;

          hence [p, q] in R iff p reduces_to (q,P,T) by A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set A = ( NonZero ( Polynom-Ring (n,L))), B = the carrier of ( Polynom-Ring (n,L));

        let R1,R2 be Relation of ( NonZero ( Polynom-Ring (n,L))), the carrier of ( Polynom-Ring (n,L)) such that

         A7: for p,q be Polynomial of n, L holds [p, q] in R1 iff p reduces_to (q,P,T) and

         A8: for p,q be Polynomial of n, L holds [p, q] in R2 iff p reduces_to (q,P,T);

        for p,q be object holds [p, q] in R1 iff [p, q] in R2

        proof

          let p,q be object;

          

           A9: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

           A10:

          now

            assume

             A11: [p, q] in R2;

            then

            consider p9,q9 be object such that

             A12: [p, q] = [p9, q9] and

             A13: p9 in A and

             A14: q9 in B by RELSET_1: 2;

            reconsider p9, q9 as Polynomial of n, L by A13, A14, POLYNOM1:def 11;

             not p9 in {( 0_ (n,L))} by A9, A13, XBOOLE_0:def 5;

            then p9 <> ( 0_ (n,L)) by TARSKI:def 1;

            then

            reconsider p9 as non-zero Polynomial of n, L by POLYNOM7:def 1;

            

             A15: p = p9 by A12, XTUPLE_0: 1;

            

             A16: q = q9 by A12, XTUPLE_0: 1;

            p9 reduces_to (q9,P,T) by A8, A11, A12;

            hence [p, q] in R1 by A7, A15, A16;

          end;

          now

            assume

             A17: [p, q] in R1;

            then

            consider p9,q9 be object such that

             A18: [p, q] = [p9, q9] and

             A19: p9 in A and

             A20: q9 in B by RELSET_1: 2;

            reconsider p9, q9 as Polynomial of n, L by A19, A20, POLYNOM1:def 11;

             not p9 in {( 0_ (n,L))} by A9, A19, XBOOLE_0:def 5;

            then p9 <> ( 0_ (n,L)) by TARSKI:def 1;

            then

            reconsider p9 as non-zero Polynomial of n, L by POLYNOM7:def 1;

            

             A21: p = p9 by A18, XTUPLE_0: 1;

            

             A22: q = q9 by A18, XTUPLE_0: 1;

            p9 reduces_to (q9,P,T) by A7, A17, A18;

            hence [p, q] in R2 by A8, A21, A22;

          end;

          hence thesis by A10;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    

     Lm18: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g,p be Polynomial of n, L st f reduces_to (g,p,T) holds f <> ( 0_ (n,L)) & p <> ( 0_ (n,L))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,g,p be Polynomial of n, L;

      assume f reduces_to (g,p,T);

      then ex b be bag of n st f reduces_to (g,p,b,T);

      hence thesis;

    end;

    theorem :: POLYRED:44

    for n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,g be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) reduces (f,g) implies g <= (f,T) & (g = ( 0_ (n,L)) or ( HT (g,T)) <= (( HT (f,T)),T))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, f,g be Polynomial of n, L, P be Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      defpred P[ Nat] means for f,g be Polynomial of n, L st ( PolyRedRel (P,T)) reduces (f,g) holds for p be RedSequence of R st (p . 1) = f & (p . ( len p)) = g & ( len p) = $1 holds g <= (f,T);

      assume

       A1: ( PolyRedRel (P,T)) reduces (f,g);

      then

      consider p be RedSequence of R such that

       A2: (p . 1) = f & (p . ( len p)) = g by REWRITE1:def 3;

       A3:

      now

        let k be Nat;

        assume

         A4: 1 <= k;

        thus P[k] implies P[(k + 1)]

        proof

          assume

           A5: P[k];

          now

            let f,g be Polynomial of n, L;

            assume ( PolyRedRel (P,T)) reduces (f,g);

            let p be RedSequence of R;

            assume that

             A6: (p . 1) = f and

             A7: (p . ( len p)) = g and

             A8: ( len p) = (k + 1);

            

             A9: ( dom p) = ( Seg (k + 1)) by A8, FINSEQ_1:def 3;

            then

             A10: (k + 1) in ( dom p) by FINSEQ_1: 4;

            set q = (p | ( Seg k));

            reconsider q as FinSequence by FINSEQ_1: 15;

            

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

            then

             A12: ( dom q) = ( Seg k) by A8, FINSEQ_1: 17;

            then

             A13: k in ( dom q) by A4, FINSEQ_1: 1;

            set h = (q . ( len q));

            

             A14: ( len q) = k by A8, A11, FINSEQ_1: 17;

            k in ( dom p) by A4, A9, A11, FINSEQ_1: 1;

            then [(p . k), (p . (k + 1))] in R by A10, REWRITE1:def 2;

            then

             A15: [h, g] in R by A7, A8, A14, A13, FUNCT_1: 47;

            then

            consider h9,g9 be object such that

             A16: [h, g] = [h9, g9] and

             A17: h9 in ( NonZero ( Polynom-Ring (n,L))) and g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

            

             A18: h = h9 by A16, XTUPLE_0: 1;

             A19:

            now

              let i be Nat;

              assume that

               A20: i in ( dom q) and

               A21: (i + 1) in ( dom q);

              (i + 1) <= k by A12, A21, FINSEQ_1: 1;

              then

               A22: (i + 1) <= (k + 1) by A11, XXREAL_0: 2;

              i <= k by A12, A20, FINSEQ_1: 1;

              then

               A23: i <= (k + 1) by A11, XXREAL_0: 2;

              1 <= (i + 1) by A12, A21, FINSEQ_1: 1;

              then

               A24: (i + 1) in ( dom p) by A9, A22, FINSEQ_1: 1;

              1 <= i by A12, A20, FINSEQ_1: 1;

              then i in ( dom p) by A9, A23, FINSEQ_1: 1;

              then

               A25: [(p . i), (p . (i + 1))] in R by A24, REWRITE1:def 2;

              (p . i) = (q . i) by A20, FUNCT_1: 47;

              hence [(q . i), (q . (i + 1))] in R by A21, A25, FUNCT_1: 47;

            end;

            ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

            then not h9 in {( 0_ (n,L))} by A17, XBOOLE_0:def 5;

            then h9 <> ( 0_ (n,L)) by TARSKI:def 1;

            then

            reconsider h as non-zero Polynomial of n, L by A17, A18, POLYNOM1:def 11, POLYNOM7:def 1;

            reconsider q as RedSequence of R by A4, A14, A19, REWRITE1:def 2;

            1 in ( dom q) by A4, A12, FINSEQ_1: 1;

            then

             A26: (q . 1) = f by A6, FUNCT_1: 47;

            then ( PolyRedRel (P,T)) reduces (f,h) by REWRITE1:def 3;

            then

             A27: h <= (f,T) by A5, A8, A11, A26, FINSEQ_1: 17;

            h reduces_to (g,P,T) by A15, Def13;

            then

             A28: ex r be Polynomial of n, L st r in P & h reduces_to (g,r,T);

            reconsider h as non-zero Polynomial of n, L;

            g < (h,T) by A28, Th43;

            then g <= (h,T);

            hence g <= (f,T) by A27, Th27;

          end;

          hence thesis;

        end;

      end;

      

       A29: P[1] by Th25;

      

       A30: for k be Nat st 1 <= k holds P[k] from NAT_1:sch 8( A29, A3);

      consider k be Nat such that

       A31: ( len p) = k;

      1 <= k by A31, NAT_1: 14;

      hence

       A32: g <= (f,T) by A1, A30, A2, A31;

      now

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

        then ( Support g) <> {} by POLYNOM7: 1;

        then

         A33: ( HT (g,T)) in ( Support g) by TERMORD:def 6;

        assume

         A34: not ( HT (g,T)) <= (( HT (f,T)),T);

        now

          per cases ;

            case ( HT (f,T)) = ( HT (g,T));

            hence contradiction by A34, TERMORD: 6;

          end;

            case

             A35: ( HT (f,T)) <> ( HT (g,T));

            ( HT (g,T)) <= (( HT (g,T)),T) by TERMORD: 6;

            then [( HT (g,T)), ( HT (g,T))] in T by TERMORD:def 2;

            then

             A36: ( HT (g,T)) in ( field T) by RELAT_1: 15;

            ( HT (f,T)) <= (( HT (f,T)),T) by TERMORD: 6;

            then [( HT (f,T)), ( HT (f,T))] in T by TERMORD:def 2;

            then T is_connected_in ( field T) & ( HT (f,T)) in ( field T) by RELAT_1: 15, RELAT_2:def 14;

            then [( HT (f,T)), ( HT (g,T))] in T or [( HT (g,T)), ( HT (f,T))] in T by A35, A36, RELAT_2:def 6;

            then ( HT (f,T)) <= (( HT (g,T)),T) by A34, TERMORD:def 2;

            then

             A37: ( HT (f,T)) < (( HT (g,T)),T) by A35, TERMORD:def 3;

            then f < (g,T) by Lm15;

            then f <= (g,T);

            then ( Support f) = ( Support g) by A32, Th26;

            then ( HT (g,T)) <= (( HT (f,T)),T) by A33, TERMORD:def 6;

            hence contradiction by A37, TERMORD: 5;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    registration

      let n be Nat, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      cluster ( PolyRedRel (P,T)) -> strongly-normalizing;

      coherence

      proof

        set BT = RelStr (# ( Bags n), T #), X = the InternalRel of ( FinPoset BT);

        set R = ( PolyRedRel (P,T));

        

         A1: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

        ( FinPoset BT) is well_founded by BAGORDER: 41;

        then

         A2: the InternalRel of ( FinPoset BT) is_well_founded_in the carrier of ( FinPoset BT) by WELLFND1:def 2;

        now

          let Y be set;

          assume that

           A3: Y c= ( field (R ~ )) and

           A4: Y <> {} ;

          set z = the Element of Y;

          z in Y by A4;

          then z in ( field (R ~ )) by A3;

          then

           A5: z in (( dom (R ~ )) \/ ( rng (R ~ ))) by RELAT_1:def 6;

          now

            per cases by A5, XBOOLE_0:def 3;

              case z in ( dom (R ~ ));

              hence z in the carrier of ( Polynom-Ring (n,L));

            end;

              case z in ( rng (R ~ ));

              hence z in the carrier of ( Polynom-Ring (n,L)) by XBOOLE_0:def 5;

            end;

          end;

          then

          reconsider z9 = z as Polynomial of n, L by POLYNOM1:def 11;

          set M = { ( Support y9) where y9 be Polynomial of n, L : ex y be set st y in Y & y9 = y };

          ( Support z9) in M by A4;

          then

          reconsider M as non empty set;

          now

            let u be object;

            assume u in M;

            then

             A6: ex p be Polynomial of n, L st ( Support p) = u & ex y be set st y in Y & p = y;

            ( FinPoset BT) = RelStr (# ( Fin the carrier of BT), ( FinOrd BT) #) by BAGORDER:def 16;

            hence u in the carrier of ( FinPoset BT) by A6, FINSUB_1:def 5;

          end;

          then M c= the carrier of ( FinPoset BT) by TARSKI:def 3;

          then

          consider a be object such that

           A7: a in M and

           A8: (X -Seg a) misses M by A2, WELLORD1:def 3;

          consider p be Polynomial of n, L such that

           A9: ( Support p) = a and

           A10: ex y be set st y in Y & p = y by A7;

          (((R ~ ) -Seg p) /\ Y) = {}

          proof

            set b = the Element of (((R ~ ) -Seg p) /\ Y);

            

             A11: ( FinPoset BT) = RelStr (# ( Fin the carrier of BT), ( FinOrd BT) #) by BAGORDER:def 16;

            assume

             A12: (((R ~ ) -Seg p) /\ Y) <> {} ;

            then b in ((R ~ ) -Seg p) by XBOOLE_0:def 4;

            then [b, p] in (R ~ ) by WELLORD1: 1;

            then

             A13: [p, b] in R by RELAT_1:def 7;

            then

            consider h9,g9 be object such that

             A14: [p, b] = [h9, g9] and

             A15: h9 in ( NonZero ( Polynom-Ring (n,L))) and

             A16: g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

            b = g9 by A14, XTUPLE_0: 1;

            then

            reconsider b9 = b as Polynomial of n, L by A16, POLYNOM1:def 11;

            

             A17: p = h9 by A14, XTUPLE_0: 1;

             not h9 in {( 0_ (n,L))} by A1, A15, XBOOLE_0:def 5;

            then h9 <> ( 0_ (n,L)) by TARSKI:def 1;

            then

            reconsider p as non-zero Polynomial of n, L by A17, POLYNOM7:def 1;

            p reduces_to (b9,P,T) by A13, Def13;

            then

             A18: ex u be Polynomial of n, L st u in P & p reduces_to (b9,u,T);

            reconsider p as non-zero Polynomial of n, L;

            

             A19: b9 < (p,T) by A18, Th43;

            then

             A20: ( Support b9) <> ( Support p);

            b in Y by A12, XBOOLE_0:def 4;

            then

             A21: ( Support b9) in M;

            b9 <= (p,T) by A19;

            then [( Support b9), ( Support p)] in X by A11;

            then ( Support b9) in (X -Seg ( Support p)) by A20, WELLORD1: 1;

            then ( Support b9) in ((X -Seg a) /\ M) by A9, A21, XBOOLE_0:def 4;

            hence contradiction by A8, XBOOLE_0:def 7;

          end;

          then ((R ~ ) -Seg p) misses Y by XBOOLE_0:def 7;

          hence ex p be object st p in Y & ((R ~ ) -Seg p) misses Y by A10;

        end;

        then (R ~ ) is well_founded by WELLORD1:def 2;

        then

         A22: R is co-well_founded by REWRITE1:def 13;

        now

          set A = (the carrier of ( Polynom-Ring (n,L)) \ {( 0_ (n,L))}), B = the carrier of ( Polynom-Ring (n,L));

          let x be object;

          assume x in ( field R);

          then

           A23: x in (( dom R) \/ ( rng R)) by RELAT_1:def 6;

          now

            per cases by A23, XBOOLE_0:def 3;

              case x in ( dom R);

              then x in B by XBOOLE_0:def 5;

              hence x is Polynomial of n, L by POLYNOM1:def 11;

            end;

              case x in ( rng R);

              hence x is Polynomial of n, L by POLYNOM1:def 11;

            end;

          end;

          then

          reconsider x9 = x as Polynomial of n, L;

          now

            assume

             A24: [x, x] in R;

            then

            consider x1,y1 be object such that

             A25: [x, x] = [x1, y1] and

             A26: x1 in A and y1 in B by A1, RELSET_1: 2;

            x = x1 by A25, XTUPLE_0: 1;

            then not x9 in {( 0_ (n,L))} by A26, XBOOLE_0:def 5;

            then x9 <> ( 0_ (n,L)) by TARSKI:def 1;

            then

            reconsider x9 as non-zero Polynomial of n, L by POLYNOM7:def 1;

            x9 reduces_to (x9,P,T) by A24, Def13;

            then ex p be Polynomial of n, L st p in P & x9 reduces_to (x9,p,T);

            then x9 < (x9,T) by Th43;

            then ( Support x9) <> ( Support x9);

            hence contradiction;

          end;

          hence not [x, x] in R;

        end;

        then R is_irreflexive_in ( field R) by RELAT_2:def 2;

        then R is irreflexive by RELAT_2:def 10;

        hence thesis by A22;

      end;

    end

    theorem :: POLYRED:45

    

     Th45: for n be Nat, T be admissible connected TermOrder of n, L be add-associative right_complementable left_zeroed right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,h be Polynomial of n, L holds f in P implies ( PolyRedRel (P,T)) reduces ((h *' f),( 0_ (n,L)))

    proof

      let n be Nat, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed left_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f9,h9 be Polynomial of n, L;

      assume

       A1: f9 in P;

      per cases ;

        suppose h9 = ( 0_ (n,L));

        then (h9 *' f9) = ( 0_ (n,L)) by Th5;

        hence thesis by REWRITE1: 12;

      end;

        suppose h9 <> ( 0_ (n,L));

        then

        reconsider h = h9 as non-zero Polynomial of n, L by POLYNOM7:def 1;

        set H = { g where g be Polynomial of n, L : not (( PolyRedRel (P,T)) reduces ((g *' f9),( 0_ (n,L)))) };

        now

          per cases ;

            case f9 = ( 0_ (n,L));

            then (h9 *' f9) = ( 0_ (n,L)) by POLYNOM1: 28;

            hence thesis by REWRITE1: 12;

          end;

            case f9 <> ( 0_ (n,L));

            then

            reconsider f = f9 as non-zero Polynomial of n, L by POLYNOM7:def 1;

             A2:

            now

              let u be object;

              assume u in H;

              then ex g9 be Polynomial of n, L st u = g9 & not ( PolyRedRel (P,T)) reduces ((g9 *' f),( 0_ (n,L)));

              hence u in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            end;

            assume not ( PolyRedRel (P,T)) reduces ((h9 *' f9),( 0_ (n,L)));

            then h in H;

            then

            reconsider H as non empty Subset of ( Polynom-Ring (n,L)) by A2, TARSKI:def 3;

            now

              assume H <> {} ;

              reconsider H as non empty set;

              consider m be Polynomial of n, L such that

               A3: m in H and

               A4: for m9 be Polynomial of n, L st m9 in H holds m <= (m9,T) by Th31;

              m <> ( 0_ (n,L))

              proof

                assume m = ( 0_ (n,L));

                then

                 A5: (m *' f) = ( 0_ (n,L)) by Th5;

                ex g9 be Polynomial of n, L st m = g9 & not ( PolyRedRel (P,T)) reduces ((g9 *' f),( 0_ (n,L))) by A3;

                hence contradiction by A5, REWRITE1: 12;

              end;

              then

              reconsider m as non-zero Polynomial of n, L by POLYNOM7:def 1;

              ( Red (m,T)) < (m,T) by Th35;

              then not m <= (( Red (m,T)),T) by Th29;

              then not ( Red (m,T)) in H by A4;

              then

               A6: ( PolyRedRel (P,T)) reduces ((( Red (m,T)) *' f),( 0_ (n,L)));

              set g = ((m *' f) - ((((m *' f) . ( HT ((m *' f),T))) / ( HC (f,T))) * (( HT (m,T)) *' f)));

              

               A7: (m *' f) <> ( 0_ (n,L)) by POLYNOM7:def 1;

              

               A8: ( HC (f,T)) <> ( 0. L);

              (m *' f) <> ( 0_ (n,L)) by POLYNOM7:def 1;

              then ( Support (m *' f)) <> {} by POLYNOM7: 1;

              then

               A9: ( HT ((m *' f),T)) in ( Support (m *' f)) by TERMORD:def 6;

              ((((m *' f) . ( HT ((m *' f),T))) / ( HC (f,T))) * (( HT (m,T)) *' f)) = ((( HC ((m *' f),T)) / ( HC (f,T))) * (( HT (m,T)) *' f)) by TERMORD:def 7

              .= (((( HC (m,T)) * ( HC (f,T))) / ( HC (f,T))) * (( HT (m,T)) *' f)) by TERMORD: 32

              .= (((( HC (m,T)) * ( HC (f,T))) * (( HC (f,T)) " )) * (( HT (m,T)) *' f))

              .= ((( HC (m,T)) * (( HC (f,T)) * (( HC (f,T)) " ))) * (( HT (m,T)) *' f)) by GROUP_1:def 3

              .= ((( HC (m,T)) * ( 1. L)) * (( HT (m,T)) *' f)) by A8, VECTSP_1:def 10

              .= (( HC (m,T)) * (( HT (m,T)) *' f))

              .= (( Monom (( HC (m,T)),( HT (m,T)))) *' f) by Th22

              .= (( HM (m,T)) *' f) by TERMORD:def 8;

              

              then

               A10: g = ((m *' f) + ( - (( HM (m,T)) *' f))) by POLYNOM1:def 7

              .= ((f *' m) + (f *' ( - ( HM (m,T))))) by Th6

              .= ((m + ( - ( HM (m,T)))) *' f) by POLYNOM1: 26

              .= ((m - ( HM (m,T))) *' f) by POLYNOM1:def 7

              .= (( Red (m,T)) *' f) by TERMORD:def 9;

              ( HT ((m *' f),T)) = (( HT (m,T)) + ( HT (f,T))) & f <> ( 0_ (n,L)) by POLYNOM7:def 1, TERMORD: 31;

              then (m *' f) reduces_to (g,f,( HT ((m *' f),T)),T) by A9, A7;

              then (m *' f) reduces_to ((( Red (m,T)) *' f),f,T) by A10;

              then (m *' f) reduces_to ((( Red (m,T)) *' f),P,T) by A1;

              then [(m *' f), (( Red (m,T)) *' f)] in ( PolyRedRel (P,T)) by Def13;

              then

               A11: ( PolyRedRel (P,T)) reduces ((m *' f),(( Red (m,T)) *' f)) by REWRITE1: 15;

              ex u be Polynomial of n, L st m = u & not ( PolyRedRel (P,T)) reduces ((u *' f),( 0_ (n,L))) by A3;

              hence contradiction by A11, A6, REWRITE1: 16;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: POLYRED:46

    

     Th46: for n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L, m be non-zero Monomial of n, L holds f reduces_to (g,P,T) implies (m *' f) reduces_to ((m *' g),P,T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L, m be non-zero Monomial of n, L;

      assume f reduces_to (g,P,T);

      then

      consider p be Polynomial of n, L such that

       A1: p in P and

       A2: f reduces_to (g,p,T);

      consider b be bag of n such that

       A3: f reduces_to (g,p,b,T) by A2;

      set b9 = (b + ( HT (m,T)));

      

       A4: b in ( Support f) by A3;

       A5:

      now

        m <> ( 0_ (n,L)) by POLYNOM7:def 1;

        then ( Support m) <> {} by POLYNOM7: 1;

        then

         A6: (m . ( term m)) <> ( 0. L) by POLYNOM7:def 5;

        assume

         A7: ((m *' f) . b9) = ( 0. L);

        ((m *' f) . b9) = ((m *' f) . (( term m) + b)) by TERMORD: 23

        .= ((m . ( term m)) * (f . b)) by Th7;

        then (f . b) = ( 0. L) by A7, A6, VECTSP_2:def 1;

        hence contradiction by A4, POLYNOM1:def 4;

      end;

      b9 is Element of ( Bags n) by PRE_POLY:def 12;

      then

       A8: b9 in ( Support (m *' f)) by A5, POLYNOM1:def 4;

      

       A9: p <> ( 0_ (n,L)) by A2, Lm18;

      consider s be bag of n such that

       A10: (s + ( HT (p,T))) = b and

       A11: g = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A3;

      reconsider p as non-zero Polynomial of n, L by A9, POLYNOM7:def 1;

      

       A12: ((s + ( HT (m,T))) + ( HT (p,T))) = b9 by A10, PRE_POLY: 35;

      set t = (s + ( HT (m,T)));

      set h = ((m *' f) - ((((m *' f) . b9) / ( HC (p,T))) * (t *' p)));

      f <> ( 0_ (n,L)) by A3;

      then

      reconsider f as non-zero Polynomial of n, L by POLYNOM7:def 1;

      (m *' f) <> ( 0_ (n,L)) & p <> ( 0_ (n,L)) by POLYNOM7:def 1;

      then (m *' f) reduces_to (h,p,b9,T) by A8, A12;

      then

       A13: (m *' f) reduces_to (h,p,T);

      

       A14: ((m . ( term m)) * ((f . b) / ( HC (p,T)))) = ((m . ( term m)) * ((f . b) * (( HC (p,T)) " )))

      .= (((m . ( term m)) * (f . b)) * (( HC (p,T)) " )) by GROUP_1:def 3

      .= (((m . ( term m)) * (f . b)) / ( HC (p,T)));

      ((m *' f) . b9) = ((m *' f) . (( term m) + b)) by TERMORD: 23

      .= ((m . ( term m)) * (f . b)) by Th7;

      

      then h = ((m *' f) - (((m . ( term m)) * ((f . b) / ( HC (p,T)))) * (( HT (m,T)) *' (s *' p)))) by A14, Th18

      .= ((m *' f) - (((f . b) / ( HC (p,T))) * ((m . ( term m)) * (( HT (m,T)) *' (s *' p))))) by Th11

      .= ((m *' f) - (((f . b) / ( HC (p,T))) * (( Monom ((m . ( term m)),( HT (m,T)))) *' (s *' p)))) by Th22

      .= ((m *' f) - (((f . b) / ( HC (p,T))) * (( Monom (( coefficient m),( term m))) *' (s *' p)))) by TERMORD: 23

      .= ((m *' f) - (((f . b) / ( HC (p,T))) * (m *' (s *' p)))) by POLYNOM7: 11

      .= ((m *' f) - (m *' (((f . b) / ( HC (p,T))) * (s *' p)))) by Th12

      .= ((m *' f) + ( - (m *' (((f . b) / ( HC (p,T))) * (s *' p))))) by POLYNOM1:def 7

      .= ((m *' f) + (m *' ( - (((f . b) / ( HC (p,T))) * (s *' p))))) by Th6

      .= (m *' (f + ( - (((f . b) / ( HC (p,T))) * (s *' p))))) by POLYNOM1: 26

      .= (m *' (f - (((f . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1:def 7;

      hence thesis by A1, A11, A13;

    end;

    theorem :: POLYRED:47

    

     Th47: for n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L, m be Monomial of n, L holds ( PolyRedRel (P,T)) reduces (f,g) implies ( PolyRedRel (P,T)) reduces ((m *' f),(m *' g))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L, m be Monomial of n, L;

      assume

       A1: ( PolyRedRel (P,T)) reduces (f,g);

      set R = ( PolyRedRel (P,T));

      per cases ;

        suppose

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

        

        then (m *' f) = ( 0_ (n,L)) by Th5

        .= (m *' g) by A2, Th5;

        hence thesis by REWRITE1: 12;

      end;

        suppose m <> ( 0_ (n,L));

        then

        reconsider m as non-zero Monomial of n, L by POLYNOM7:def 1;

        defpred P[ Nat] means for f,g be Polynomial of n, L st ( PolyRedRel (P,T)) reduces (f,g) holds for p be RedSequence of R st (p . 1) = f & (p . ( len p)) = g & ( len p) = $1 holds ( PolyRedRel (P,T)) reduces ((m *' f),(m *' g));

        consider p be RedSequence of R such that

         A3: (p . 1) = f & (p . ( len p)) = g by A1, REWRITE1:def 3;

        consider k be Nat such that

         A4: ( len p) = k;

         A5:

        now

          let k be Nat;

          assume

           A6: 1 <= k;

          thus P[k] implies P[(k + 1)]

          proof

            assume

             A7: P[k];

            now

              let f,g be Polynomial of n, L;

              assume ( PolyRedRel (P,T)) reduces (f,g);

              let p be RedSequence of R;

              assume that

               A8: (p . 1) = f and

               A9: (p . ( len p)) = g and

               A10: ( len p) = (k + 1);

              

               A11: ( dom p) = ( Seg (k + 1)) by A10, FINSEQ_1:def 3;

              then

               A12: (k + 1) in ( dom p) by FINSEQ_1: 4;

              set q = (p | ( Seg k));

              reconsider q as FinSequence by FINSEQ_1: 15;

              

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

              then

               A14: ( dom q) = ( Seg k) by A10, FINSEQ_1: 17;

              then

               A15: k in ( dom q) by A6, FINSEQ_1: 1;

              set h = (q . ( len q));

              

               A16: ( len q) = k by A10, A13, FINSEQ_1: 17;

              k in ( dom p) by A6, A11, A13, FINSEQ_1: 1;

              then [(p . k), (p . (k + 1))] in R by A12, REWRITE1:def 2;

              then

               A17: [h, g] in R by A9, A10, A16, A15, FUNCT_1: 47;

              then

              consider h9,g9 be object such that

               A18: [h, g] = [h9, g9] and

               A19: h9 in ( NonZero ( Polynom-Ring (n,L))) and g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

              

               A20: h = h9 by A18, XTUPLE_0: 1;

               A21:

              now

                let i be Nat;

                assume that

                 A22: i in ( dom q) and

                 A23: (i + 1) in ( dom q);

                (i + 1) <= k by A14, A23, FINSEQ_1: 1;

                then

                 A24: (i + 1) <= (k + 1) by A13, XXREAL_0: 2;

                i <= k by A14, A22, FINSEQ_1: 1;

                then

                 A25: i <= (k + 1) by A13, XXREAL_0: 2;

                1 <= (i + 1) by A14, A23, FINSEQ_1: 1;

                then

                 A26: (i + 1) in ( dom p) by A11, A24, FINSEQ_1: 1;

                1 <= i by A14, A22, FINSEQ_1: 1;

                then i in ( dom p) by A11, A25, FINSEQ_1: 1;

                then

                 A27: [(p . i), (p . (i + 1))] in R by A26, REWRITE1:def 2;

                (p . i) = (q . i) by A22, FUNCT_1: 47;

                hence [(q . i), (q . (i + 1))] in R by A23, A27, FUNCT_1: 47;

              end;

              ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

              then not h9 in {( 0_ (n,L))} by A19, XBOOLE_0:def 5;

              then h9 <> ( 0_ (n,L)) by TARSKI:def 1;

              then

              reconsider h as non-zero Polynomial of n, L by A19, A20, POLYNOM1:def 11, POLYNOM7:def 1;

              h reduces_to (g,P,T) by A17, Def13;

              then (m *' h) reduces_to ((m *' g),P,T) by Th46;

              then [(m *' h), (m *' g)] in ( PolyRedRel (P,T)) by Def13;

              then

               A28: ( PolyRedRel (P,T)) reduces ((m *' h),(m *' g)) by REWRITE1: 15;

              reconsider q as RedSequence of R by A6, A16, A21, REWRITE1:def 2;

              1 in ( dom q) by A6, A14, FINSEQ_1: 1;

              then

               A29: (q . 1) = f by A8, FUNCT_1: 47;

              then ( PolyRedRel (P,T)) reduces (f,h) by REWRITE1:def 3;

              then ( PolyRedRel (P,T)) reduces ((m *' f),(m *' h)) by A7, A10, A13, A29, FINSEQ_1: 17;

              hence ( PolyRedRel (P,T)) reduces ((m *' f),(m *' g)) by A28, REWRITE1: 16;

            end;

            hence thesis;

          end;

        end;

        

         A30: P[1] by REWRITE1: 12;

        

         A31: for k be Nat st 1 <= k holds P[k] from NAT_1:sch 8( A30, A5);

        1 <= k by A4, NAT_1: 14;

        hence thesis by A1, A31, A3, A4;

      end;

    end;

    theorem :: POLYRED:48

    for n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f be Polynomial of n, L, m be Monomial of n, L holds ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L))) implies ( PolyRedRel (P,T)) reduces ((m *' f),( 0_ (n,L)))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f be Polynomial of n, L, m be Monomial of n, L;

      assume ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L)));

      then ( PolyRedRel (P,T)) reduces ((m *' f),(m *' ( 0_ (n,L)))) by Th47;

      hence thesis by POLYNOM1: 28;

    end;

    theorem :: POLYRED:49

    

     Th49: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g,h,h1 be Polynomial of n, L holds ((f - g) = h & ( PolyRedRel (P,T)) reduces (h,h1)) implies ex f1,g1 be Polynomial of n, L st (f1 - g1) = h1 & ( PolyRedRel (P,T)) reduces (f,f1) & ( PolyRedRel (P,T)) reduces (g,g1)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g,h,h1 be Polynomial of n, L;

      assume that

       A1: (f - g) = h and

       A2: ( PolyRedRel (P,T)) reduces (h,h1);

      consider p be RedSequence of ( PolyRedRel (P,T)) such that

       A3: (p . 1) = h & (p . ( len p)) = h1 by A2, REWRITE1:def 3;

      defpred P[ Nat] means for f,g,h be Polynomial of n, L st (f - g) = h holds for h1 be Polynomial of n, L holds for p be RedSequence of ( PolyRedRel (P,T)) st (p . 1) = h & (p . ( len p)) = h1 & ( len p) = $1 holds ex f1,g1 be Polynomial of n, L st (f1 - g1) = h1 & ( PolyRedRel (P,T)) reduces (f,f1) & ( PolyRedRel (P,T)) reduces (g,g1);

       A4:

      now

        let k be Nat;

        assume

         A5: 1 <= k;

        assume

         A6: P[k];

        thus P[(k + 1)]

        proof

          let f,g,h be Polynomial of n, L;

          assume

           A7: (f - g) = h;

          let h1 be Polynomial of n, L;

          let r be RedSequence of ( PolyRedRel (P,T));

          assume that

           A8: (r . 1) = h and

           A9: (r . ( len r)) = h1 and

           A10: ( len r) = (k + 1);

          set h2 = (r . k);

          

           A11: ( dom r) = ( Seg (k + 1)) by A10, FINSEQ_1:def 3;

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

          then

           A12: (k + 1) in ( dom r) by A11, FINSEQ_1: 1;

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

          then k in ( dom r) by A5, A11, FINSEQ_1: 1;

          then

           A13: [(r . k), (r . (k + 1))] in ( PolyRedRel (P,T)) by A12, REWRITE1:def 2;

          then

          consider x,y be object such that

           A14: x in ( NonZero ( Polynom-Ring (n,L))) and y in the carrier of ( Polynom-Ring (n,L)) and

           A15: [(r . k), (r . (k + 1))] = [x, y] by ZFMISC_1:def 2;

          

           A16: (r . k) = x by A15, XTUPLE_0: 1;

          then

          reconsider h2 as Polynomial of n, L by A14, POLYNOM1:def 11;

          ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

          then not (r . k) in {( 0_ (n,L))} by A14, A16, XBOOLE_0:def 5;

          then (r . k) <> ( 0_ (n,L)) by TARSKI:def 1;

          then

          reconsider h2 as non-zero Polynomial of n, L by POLYNOM7:def 1;

          h2 reduces_to (h1,P,T) by A9, A10, A13, Def13;

          then

          consider p be Polynomial of n, L such that

           A17: p in P and

           A18: h2 reduces_to (h1,p,T);

          consider b be bag of n such that

           A19: h2 reduces_to (h1,p,b,T) by A18;

          set q = (r | ( Seg k));

          reconsider q as FinSequence by FINSEQ_1: 15;

          

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

          then

           A21: ( dom q) = ( Seg k) by A10, FINSEQ_1: 17;

          

           A22: ( dom r) = ( Seg (k + 1)) by A10, FINSEQ_1:def 3;

           A23:

          now

            let i be Nat;

            assume that

             A24: i in ( dom q) and

             A25: (i + 1) in ( dom q);

            (i + 1) <= k by A21, A25, FINSEQ_1: 1;

            then

             A26: (i + 1) <= (k + 1) by A20, XXREAL_0: 2;

            i <= k by A21, A24, FINSEQ_1: 1;

            then

             A27: i <= (k + 1) by A20, XXREAL_0: 2;

            1 <= (i + 1) by A21, A25, FINSEQ_1: 1;

            then

             A28: (i + 1) in ( dom r) by A22, A26, FINSEQ_1: 1;

            1 <= i by A21, A24, FINSEQ_1: 1;

            then i in ( dom r) by A22, A27, FINSEQ_1: 1;

            then

             A29: [(r . i), (r . (i + 1))] in ( PolyRedRel (P,T)) by A28, REWRITE1:def 2;

            (r . i) = (q . i) by A24, FUNCT_1: 47;

            hence [(q . i), (q . (i + 1))] in ( PolyRedRel (P,T)) by A25, A29, FUNCT_1: 47;

          end;

          ( len q) = k by A10, A20, FINSEQ_1: 17;

          then

          reconsider q as RedSequence of ( PolyRedRel (P,T)) by A5, A23, REWRITE1:def 2;

          

           A30: k in ( dom q) by A5, A21, FINSEQ_1: 1;

          1 in ( dom q) by A5, A21, FINSEQ_1: 1;

          then

           A31: (q . 1) = h by A8, FUNCT_1: 47;

          (q . ( len q)) = (q . k) by A10, A20, FINSEQ_1: 17

          .= h2 by A30, FUNCT_1: 47;

          then

          consider f2,g2 be Polynomial of n, L such that

           A32: (f2 - g2) = h2 and

           A33: ( PolyRedRel (P,T)) reduces (f,f2) and

           A34: ( PolyRedRel (P,T)) reduces (g,g2) by A6, A7, A10, A20, A31, FINSEQ_1: 17;

          consider s be bag of n such that

           A35: (s + ( HT (p,T))) = b and

           A36: h1 = (h2 - (((h2 . b) / ( HC (p,T))) * (s *' p))) by A19;

          set f1 = (f2 - (((f2 . b) / ( HC (p,T))) * (s *' p))), g1 = (g2 - (((g2 . b) / ( HC (p,T))) * (s *' p)));

          

           A37: (((f2 . b) / ( HC (p,T))) + ( - ((g2 . b) / ( HC (p,T))))) = (((f2 . b) * (( HC (p,T)) " )) + ( - ((g2 . b) / ( HC (p,T)))))

          .= (((f2 . b) * (( HC (p,T)) " )) + ( - ((g2 . b) * (( HC (p,T)) " ))))

          .= (((f2 . b) * (( HC (p,T)) " )) + (( - (g2 . b)) * (( HC (p,T)) " ))) by VECTSP_1: 9

          .= (((f2 . b) + ( - (g2 . b))) * (( HC (p,T)) " )) by VECTSP_1:def 7

          .= (((f2 . b) + (( - g2) . b)) * (( HC (p,T)) " )) by POLYNOM1: 17

          .= (((f2 + ( - g2)) . b) * (( HC (p,T)) " )) by POLYNOM1: 15

          .= (((f2 - g2) . b) * (( HC (p,T)) " )) by POLYNOM1:def 7

          .= (((f2 - g2) . b) / ( HC (p,T)));

           A38:

          now

            per cases ;

              case

               A39: not b in ( Support g2);

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

              then (g2 . b) = ( 0. L) by A39, POLYNOM1:def 4;

              

              then g1 = (g2 - ((( 0. L) * (( HC (p,T)) " )) * (s *' p)))

              .= (g2 - (( 0. L) * (s *' p)))

              .= (g2 - ( 0_ (n,L))) by Th8

              .= g2 by Th4;

              hence ( PolyRedRel (P,T)) reduces (g,g1) by A34;

            end;

              case

               A40: b in ( Support g2);

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

              then

              reconsider g2 as non-zero Polynomial of n, L by POLYNOM7:def 1;

              g2 <> ( 0_ (n,L)) & p <> ( 0_ (n,L)) by A18, Lm18, POLYNOM7:def 1;

              then g2 reduces_to (g1,p,b,T) by A35, A40;

              then g2 reduces_to (g1,p,T);

              then g2 reduces_to (g1,P,T) by A17;

              then [g2, g1] in ( PolyRedRel (P,T)) by Def13;

              then ( PolyRedRel (P,T)) reduces (g2,g1) by REWRITE1: 15;

              hence ( PolyRedRel (P,T)) reduces (g,g1) by A34, REWRITE1: 16;

            end;

          end;

           A41:

          now

            per cases ;

              case

               A42: not b in ( Support f2);

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

              then (f2 . b) = ( 0. L) by A42, POLYNOM1:def 4;

              

              then f1 = (f2 - ((( 0. L) * (( HC (p,T)) " )) * (s *' p)))

              .= (f2 - (( 0. L) * (s *' p)))

              .= (f2 - ( 0_ (n,L))) by Th8

              .= f2 by Th4;

              hence ( PolyRedRel (P,T)) reduces (f,f1) by A33;

            end;

              case

               A43: b in ( Support f2);

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

              then

              reconsider f2 as non-zero Polynomial of n, L by POLYNOM7:def 1;

              f2 <> ( 0_ (n,L)) & p <> ( 0_ (n,L)) by A18, Lm18, POLYNOM7:def 1;

              then f2 reduces_to (f1,p,b,T) by A35, A43;

              then f2 reduces_to (f1,p,T);

              then f2 reduces_to (f1,P,T) by A17;

              then [f2, f1] in ( PolyRedRel (P,T)) by Def13;

              then ( PolyRedRel (P,T)) reduces (f2,f1) by REWRITE1: 15;

              hence ( PolyRedRel (P,T)) reduces (f,f1) by A33, REWRITE1: 16;

            end;

          end;

          

           A44: ( - ( - (((g2 . b) / ( HC (p,T))) * (s *' p)))) = (((g2 . b) / ( HC (p,T))) * (s *' p)) by POLYNOM1: 19;

          

           A45: ((( - ((f2 . b) / ( HC (p,T)))) * (s *' p)) + (((g2 . b) / ( HC (p,T))) * (s *' p))) = ((( - ((f2 . b) / ( HC (p,T)))) + ((g2 . b) / ( HC (p,T)))) * (s *' p)) by Th10

          .= ( - ( - ((( - ((f2 . b) / ( HC (p,T)))) + ((g2 . b) / ( HC (p,T)))) * (s *' p)))) by POLYNOM1: 19;

          (f1 - g1) = ((f2 - (((f2 . b) / ( HC (p,T))) * (s *' p))) + ( - (g2 - (((g2 . b) / ( HC (p,T))) * (s *' p))))) by POLYNOM1:def 7

          .= ((f2 + ( - (((f2 . b) / ( HC (p,T))) * (s *' p)))) + ( - (g2 - (((g2 . b) / ( HC (p,T))) * (s *' p))))) by POLYNOM1:def 7

          .= ((f2 + ( - (((f2 . b) / ( HC (p,T))) * (s *' p)))) + ( - (g2 + ( - (((g2 . b) / ( HC (p,T))) * (s *' p)))))) by POLYNOM1:def 7

          .= ((f2 + ( - (((f2 . b) / ( HC (p,T))) * (s *' p)))) + (( - g2) + ( - ( - (((g2 . b) / ( HC (p,T))) * (s *' p)))))) by Th1

          .= (((f2 + ( - (((f2 . b) / ( HC (p,T))) * (s *' p)))) + ( - g2)) + (((g2 . b) / ( HC (p,T))) * (s *' p))) by A44, POLYNOM1: 21

          .= ((( - (((f2 . b) / ( HC (p,T))) * (s *' p))) + (f2 + ( - g2))) + (((g2 . b) / ( HC (p,T))) * (s *' p))) by POLYNOM1: 21

          .= ((f2 + ( - g2)) + (( - (((f2 . b) / ( HC (p,T))) * (s *' p))) + (((g2 . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1: 21

          .= ((f2 - g2) + (( - (((f2 . b) / ( HC (p,T))) * (s *' p))) + (((g2 . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1:def 7

          .= ((f2 - g2) + ((( - ((f2 . b) / ( HC (p,T)))) * (s *' p)) + (((g2 . b) / ( HC (p,T))) * (s *' p)))) by Th9

          .= ((f2 - g2) + ( - (( - (( - ((f2 . b) / ( HC (p,T)))) + ((g2 . b) / ( HC (p,T))))) * (s *' p)))) by A45, Th9

          .= ((f2 - g2) - (( - (( - ((f2 . b) / ( HC (p,T)))) + ((g2 . b) / ( HC (p,T))))) * (s *' p))) by POLYNOM1:def 7

          .= ((f2 - g2) - ((( - ( - ((f2 . b) / ( HC (p,T))))) + ( - ((g2 . b) / ( HC (p,T))))) * (s *' p))) by RLVECT_1: 31

          .= h1 by A32, A36, A37, RLVECT_1: 17;

          hence thesis by A41, A38;

        end;

      end;

      

       A46: P[1]

      proof

        let f,g,h be Polynomial of n, L;

        assume

         A47: (f - g) = h;

        let h1 be Polynomial of n, L;

        let p be RedSequence of ( PolyRedRel (P,T));

        assume

         A48: (p . 1) = h & (p . ( len p)) = h1 & ( len p) = 1;

        take f, g;

        thus thesis by A47, A48, REWRITE1: 12;

      end;

      

       A49: for k be Nat st 1 <= k holds P[k] from NAT_1:sch 8( A46, A4);

      consider k be Nat such that

       A50: ( len p) = k;

      1 <= k by A50, NAT_1: 14;

      hence thesis by A1, A49, A3, A50;

    end;

    theorem :: POLYRED:50

    

     Th50: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L holds ( PolyRedRel (P,T)) reduces ((f - g),( 0_ (n,L))) implies (f,g) are_convergent_wrt ( PolyRedRel (P,T))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L;

      assume ( PolyRedRel (P,T)) reduces ((f - g),( 0_ (n,L)));

      then

      consider f1,g1 be Polynomial of n, L such that

       A1: (f1 - g1) = ( 0_ (n,L)) and

       A2: ( PolyRedRel (P,T)) reduces (f,f1) & ( PolyRedRel (P,T)) reduces (g,g1) by Th49;

      g1 = ((f1 - g1) + g1) by A1, Th2

      .= ((f1 + ( - g1)) + g1) by POLYNOM1:def 7

      .= (f1 + (( - g1) + g1)) by POLYNOM1: 21

      .= (f1 + ( 0_ (n,L))) by Th3

      .= f1 by POLYNOM1: 23;

      hence thesis by A2, REWRITE1:def 7;

    end;

    theorem :: POLYRED:51

    

     Th51: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L holds ( PolyRedRel (P,T)) reduces ((f - g),( 0_ (n,L))) implies (f,g) are_convertible_wrt ( PolyRedRel (P,T))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L;

      set R = ( PolyRedRel (P,T));

      assume ( PolyRedRel (P,T)) reduces ((f - g),( 0_ (n,L)));

      then (f,g) are_convergent_wrt R by Th50;

      then

      consider h be object such that

       A1: R reduces (f,h) and

       A2: R reduces (g,h) by REWRITE1:def 7;

      (R ~ ) reduces (h,g) by A2, REWRITE1: 24;

      then

       A3: (R \/ (R ~ )) reduces (h,g) by REWRITE1: 22, XBOOLE_1: 7;

      (R \/ (R ~ )) reduces (f,h) by A1, REWRITE1: 22, XBOOLE_1: 7;

      then (R \/ (R ~ )) reduces (f,g) by A3, REWRITE1: 16;

      hence thesis by REWRITE1:def 4;

    end;

    definition

      let R be non empty addLoopStr, I be Subset of R, a,b be Element of R;

      :: POLYRED:def14

      pred a,b are_congruent_mod I means (a - b) in I;

    end

    theorem :: POLYRED:52

    for R be add-associative left_zeroed right_zeroed right_complementable right-distributive non empty doubleLoopStr, I be right-ideal non empty Subset of R, a be Element of R holds (a,a) are_congruent_mod I

    proof

      let R be add-associative left_zeroed right_zeroed right_complementable right-distributive non empty doubleLoopStr, I be right-ideal non empty Subset of R, a be Element of R;

      (a - a) = ( 0. R) & ( 0. R) in I by IDEAL_1: 3, RLVECT_1: 15;

      hence thesis;

    end;

    theorem :: POLYRED:53

    

     Th53: for R be add-associative right_zeroed right_complementable well-unital right-distributive non empty doubleLoopStr, I be right-ideal non empty Subset of R, a,b be Element of R holds (a,b) are_congruent_mod I implies (b,a) are_congruent_mod I

    proof

      let R be add-associative right_zeroed right_complementable right-distributive well-unital non empty doubleLoopStr, I be right-ideal non empty Subset of R, a,b be Element of R;

      assume (a,b) are_congruent_mod I;

      then (a - b) in I;

      then

       A1: ( - (a - b)) in I by IDEAL_1: 14;

      ((b - a) - ( - (a - b))) = ((b - a) + ( - ( - (a - b))))

      .= ((b - a) + (a - b)) by RLVECT_1: 17

      .= ((b + ( - a)) + (a - b))

      .= (b + (( - a) + (a - b))) by RLVECT_1:def 3

      .= (b + (( - a) + (a + ( - b))))

      .= (b + ((( - a) + a) + ( - b))) by RLVECT_1:def 3

      .= (b + (( 0. R) + ( - b))) by RLVECT_1: 5

      .= (b + ( - b)) by ALGSTR_1:def 2

      .= ( 0. R) by RLVECT_1: 5;

      then (b - a) = ( - (a - b)) by RLVECT_1: 21;

      hence thesis by A1;

    end;

    theorem :: POLYRED:54

    

     Th54: for R be add-associative right_zeroed right_complementable non empty addLoopStr, I be add-closed non empty Subset of R, a,b,c be Element of R holds (a,b) are_congruent_mod I & (b,c) are_congruent_mod I implies (a,c) are_congruent_mod I

    proof

      let R be add-associative right_zeroed right_complementable non empty addLoopStr, I be add-closed non empty Subset of R, a,b,c be Element of R;

      assume (a,b) are_congruent_mod I & (b,c) are_congruent_mod I;

      then (a - b) in I & (b - c) in I;

      then

       A1: ((a - b) + (b - c)) in I by IDEAL_1:def 1;

      ((a - b) + (b - c)) = ((a + ( - b)) + (b - c))

      .= (a + (( - b) + (b - c))) by RLVECT_1:def 3

      .= (a + (( - b) + (b + ( - c))))

      .= (a + ((( - b) + b) + ( - c))) by RLVECT_1:def 3

      .= (a + (( 0. R) + ( - c))) by RLVECT_1: 5

      .= (a + ( - c)) by ALGSTR_1:def 2

      .= (a - c);

      hence thesis by A1;

    end;

    theorem :: POLYRED:55

    for R be Abelian add-associative right_zeroed right_complementable well-unital distributive associative non trivial doubleLoopStr, I be add-closed non empty Subset of R, a,b,c,d be Element of R holds (a,b) are_congruent_mod I & (c,d) are_congruent_mod I implies ((a + c),(b + d)) are_congruent_mod I

    proof

      let R be Abelian add-associative right_zeroed right_complementable well-unital distributive associative non trivial doubleLoopStr, I be add-closed non empty Subset of R, a,b,c,d be Element of R;

      assume (a,b) are_congruent_mod I & (c,d) are_congruent_mod I;

      then (a - b) in I & (c - d) in I;

      then

       A1: ((a - b) + (c - d)) in I by IDEAL_1:def 1;

      ((a + c) - (b + d)) = ((a + c) + ( - (b + d)))

      .= ((a + c) + (( - d) + ( - b))) by RLVECT_1: 31

      .= (a + (c + (( - d) + ( - b)))) by RLVECT_1:def 3

      .= (a + ((c + ( - d)) + ( - b))) by RLVECT_1:def 3

      .= ((a + ( - b)) + (c + ( - d))) by RLVECT_1:def 3

      .= ((a - b) + (c + ( - d)))

      .= ((a - b) + (c - d));

      hence thesis by A1;

    end;

    theorem :: POLYRED:56

    for R be add-associative right_zeroed right_complementable commutative distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, a,b,c,d be Element of R holds (a,b) are_congruent_mod I & (c,d) are_congruent_mod I implies ((a * c),(b * d)) are_congruent_mod I

    proof

      let R be add-associative right_zeroed right_complementable commutative distributive non empty doubleLoopStr, I be add-closed right-ideal non empty Subset of R, a,b,c,d be Element of R;

      assume that

       A1: (a,b) are_congruent_mod I and

       A2: (c,d) are_congruent_mod I;

      (c - d) in I by A2;

      then

       A3: ((c - d) * b) in I by IDEAL_1:def 3;

      

       A4: ((c - d) * b) = ((c + ( - d)) * b)

      .= ((c * b) + (( - d) * b)) by VECTSP_1:def 3;

      ((a - b) * c) = ((a + ( - b)) * c)

      .= ((a * c) + (( - b) * c)) by VECTSP_1:def 3;

      

      then

       A5: (((a - b) * c) + ((c - d) * b)) = ((a * c) + ((( - b) * c) + ((c * b) + (( - d) * b)))) by A4, RLVECT_1:def 3

      .= ((a * c) + (((( - b) * c) + (c * b)) + (( - d) * b))) by RLVECT_1:def 3

      .= ((a * c) + ((( - (b * c)) + (c * b)) + (( - d) * b))) by VECTSP_1: 9

      .= ((a * c) + (( 0. R) + (( - d) * b))) by RLVECT_1: 5

      .= ((a * c) + (( - d) * b)) by ALGSTR_1:def 2

      .= ((a * c) + ( - (d * b))) by VECTSP_1: 9

      .= ((a * c) - (b * d));

      (a - b) in I by A1;

      then ((a - b) * c) in I by IDEAL_1:def 3;

      then (((a - b) * c) + ((c - d) * b)) in I by A3, IDEAL_1:def 1;

      hence thesis by A5;

    end;

    

     Lm19: for n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f be non-zero Polynomial of n, L, g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L)) st f = f9 & g = g9 holds f reduces_to (g,P,T) implies (f9,g9) are_congruent_mod (P -Ideal )

    proof

      let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f be non-zero Polynomial of n, L, g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L));

      assume that

       A1: f = f9 and

       A2: g = g9;

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

      reconsider x = ( - g) as Element of R by POLYNOM1:def 11;

      reconsider x as Element of R;

      (x + g9) = (( - g) + g) by A2, POLYNOM1:def 11

      .= ( 0_ (n,L)) by Th3

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

      then

       A3: ( - g9) = ( - g) by RLVECT_1: 6;

      assume f reduces_to (g,P,T);

      then

      consider p be Polynomial of n, L such that

       A4: p in P and

       A5: f reduces_to (g,p,T);

      consider b be bag of n such that

       A6: f reduces_to (g,p,b,T) by A5;

      consider s be bag of n such that (s + ( HT (p,T))) = b and

       A7: g = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A6;

      reconsider P as non empty Subset of ( Polynom-Ring (n,L)) by A4;

      set q = (((f . b) / ( HC (p,T))) * (s *' p)), q9 = (( Monom (((f . b) / ( HC (p,T))),s)) *' p);

      set r = <*q9*>;

      now

        let u be object;

        

         A8: ( rng r) = {q9} by FINSEQ_1: 39;

        assume u in ( rng r);

        then u = q9 by A8, TARSKI:def 1;

        hence u in the carrier of R by POLYNOM1:def 11;

      end;

      then ( rng r) c= the carrier of R by TARSKI:def 3;

      then

      reconsider r as FinSequence of the carrier of R by FINSEQ_1:def 4;

      now

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

        reconsider m = ( Monom (((f . b) / ( HC (p,T))),s)) as Element of R by POLYNOM1:def 11;

        let i be set;

        assume

         A9: i in ( dom r);

        reconsider p9 as Element of R;

        reconsider m as Element of R;

        

         A10: ((m * p9) * ( 1. R)) = (m * p9)

        .= q9 by POLYNOM1:def 11;

        ( dom r) = ( Seg 1) by FINSEQ_1: 38;

        then i = 1 by A9, FINSEQ_1: 2, TARSKI:def 1;

        then (r . i) = q9 by FINSEQ_1: 40;

        hence ex u,v be Element of R, a be Element of P st (r /. i) = ((u * a) * v) by A4, A9, A10, PARTFUN1:def 6;

      end;

      then

      reconsider r as LinearCombination of P by IDEAL_1:def 8;

      q9 is Element of R by POLYNOM1:def 11;

      then

       A11: ( Sum r) = q9 by BINOM: 3;

      q9 = q by Th22;

      then

       A12: q in (P -Ideal ) by A11, IDEAL_1: 60;

      

       A13: (f - g) = (f + ( - g)) by POLYNOM1:def 7

      .= (f9 + ( - g9)) by A1, A3, POLYNOM1:def 11

      .= (f9 - g9);

      

       A14: ( - ( - (((f . b) / ( HC (p,T))) * (s *' p)))) = (((f . b) / ( HC (p,T))) * (s *' p)) by POLYNOM1: 19;

      (f - g) = (f + ( - (f - (((f . b) / ( HC (p,T))) * (s *' p))))) by A7, POLYNOM1:def 7

      .= (f + ( - (f + ( - (((f . b) / ( HC (p,T))) * (s *' p)))))) by POLYNOM1:def 7

      .= (f + (( - f) + ( - ( - (((f . b) / ( HC (p,T))) * (s *' p)))))) by Th1

      .= ((f + ( - f)) + (((f . b) / ( HC (p,T))) * (s *' p))) by A14, POLYNOM1: 21

      .= (( 0_ (n,L)) + (((f . b) / ( HC (p,T))) * (s *' p))) by Th3

      .= (((f . b) / ( HC (p,T))) * (s *' p)) by Th2;

      hence thesis by A12, A13;

    end;

    theorem :: POLYRED:57

    

     Th57: for n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Element of ( Polynom-Ring (n,L)) holds (f,g) are_convertible_wrt ( PolyRedRel (P,T)) implies (f,g) are_congruent_mod (P -Ideal )

    proof

      let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Element of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T)), PR = ( Polynom-Ring (n,L));

      defpred P[ Nat] means for f,g be Element of ( Polynom-Ring (n,L)) st (R \/ (R ~ )) reduces (f,g) holds for p be RedSequence of (R \/ (R ~ )) st (p . 1) = f & (p . ( len p)) = g & ( len p) = $1 holds (f,g) are_congruent_mod (P -Ideal );

      assume (f,g) are_convertible_wrt ( PolyRedRel (P,T));

      then

       A1: (R \/ (R ~ )) reduces (f,g) by REWRITE1:def 4;

      then

      consider p be RedSequence of (R \/ (R ~ )) such that

       A2: (p . 1) = f & (p . ( len p)) = g by REWRITE1:def 3;

      

       A3: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

       A4:

      now

        let k be Nat;

        assume

         A5: 1 <= k;

        thus P[k] implies P[(k + 1)]

        proof

          assume

           A6: P[k];

          now

            let f,g be Element of ( Polynom-Ring (n,L));

            assume (R \/ (R ~ )) reduces (f,g);

            let p be RedSequence of (R \/ (R ~ ));

            assume that

             A7: (p . 1) = f and

             A8: (p . ( len p)) = g and

             A9: ( len p) = (k + 1);

            

             A10: ( dom p) = ( Seg (k + 1)) by A9, FINSEQ_1:def 3;

            then

             A11: (k + 1) in ( dom p) by FINSEQ_1: 4;

            set q = (p | ( Seg k));

            reconsider q as FinSequence by FINSEQ_1: 15;

            

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

            then

             A13: ( dom q) = ( Seg k) by A9, FINSEQ_1: 17;

            then

             A14: k in ( dom q) by A5, FINSEQ_1: 1;

            set h = (q . ( len q));

            

             A15: ( len q) = k by A9, A12, FINSEQ_1: 17;

            k in ( dom p) by A5, A10, A12, FINSEQ_1: 1;

            then [(p . k), (p . (k + 1))] in (R \/ (R ~ )) by A11, REWRITE1:def 2;

            then [h, g] in (R \/ (R ~ )) by A8, A9, A15, A14, FUNCT_1: 47;

            then

             A16: [h, g] in R or [h, g] in (R ~ ) by XBOOLE_0:def 3;

             A17:

            now

              per cases by A16, RELAT_1:def 7;

                case [h, g] in R;

                then

                consider h9,g9 be object such that

                 A18: [h, g] = [h9, g9] and

                 A19: h9 in ( NonZero ( Polynom-Ring (n,L))) and g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                h = h9 by A18, XTUPLE_0: 1;

                hence h in (the carrier of ( Polynom-Ring (n,L)) \ {( 0_ (n,L))}) & h in the carrier of ( Polynom-Ring (n,L)) & g in the carrier of ( Polynom-Ring (n,L)) by A19, POLYNOM1:def 11;

              end;

                case [g, h] in R;

                then

                consider h9,g9 be object such that

                 A20: [g, h] = [h9, g9] and

                 A21: h9 in ( NonZero ( Polynom-Ring (n,L))) & g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                

                 A22: h = g9 by A20, XTUPLE_0: 1;

                g = h9 by A20, XTUPLE_0: 1;

                hence g in (the carrier of ( Polynom-Ring (n,L)) \ {( 0_ (n,L))}) & g in the carrier of ( Polynom-Ring (n,L)) & h in the carrier of ( Polynom-Ring (n,L)) by A21, A22, POLYNOM1:def 11;

              end;

            end;

            now

              let i be Nat;

              assume that

               A23: i in ( dom q) and

               A24: (i + 1) in ( dom q);

              (i + 1) <= k by A13, A24, FINSEQ_1: 1;

              then

               A25: (i + 1) <= (k + 1) by A12, XXREAL_0: 2;

              i <= k by A13, A23, FINSEQ_1: 1;

              then

               A26: i <= (k + 1) by A12, XXREAL_0: 2;

              1 <= (i + 1) by A13, A24, FINSEQ_1: 1;

              then

               A27: (i + 1) in ( dom p) by A10, A25, FINSEQ_1: 1;

              1 <= i by A13, A23, FINSEQ_1: 1;

              then i in ( dom p) by A10, A26, FINSEQ_1: 1;

              then

               A28: [(p . i), (p . (i + 1))] in (R \/ (R ~ )) by A27, REWRITE1:def 2;

              (p . i) = (q . i) by A23, FUNCT_1: 47;

              hence [(q . i), (q . (i + 1))] in (R \/ (R ~ )) by A24, A28, FUNCT_1: 47;

            end;

            then

            reconsider q as RedSequence of (R \/ (R ~ )) by A5, A15, REWRITE1:def 2;

            reconsider h as Polynomial of n, L by A17, POLYNOM1:def 11;

            reconsider h9 = h as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            reconsider h9 as Element of ( Polynom-Ring (n,L));

            1 in ( dom q) by A5, A13, FINSEQ_1: 1;

            then

             A29: (q . 1) = f by A7, FUNCT_1: 47;

            then (R \/ (R ~ )) reduces (f,h) by REWRITE1:def 3;

            then

             A30: (f,h9) are_congruent_mod (P -Ideal ) by A6, A9, A12, A29, FINSEQ_1: 17;

            now

              per cases by A16, RELAT_1:def 7;

                case

                 A31: [h, g] in R;

                then

                consider h9,g9 be object such that

                 A32: [h, g] = [h9, g9] and

                 A33: h9 in ( NonZero ( Polynom-Ring (n,L))) and

                 A34: g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                

                 A35: h = h9 by A32, XTUPLE_0: 1;

                 not h9 in {( 0_ (n,L))} by A3, A33, XBOOLE_0:def 5;

                then h9 <> ( 0_ (n,L)) by TARSKI:def 1;

                then

                reconsider h as non-zero Polynomial of n, L by A35, POLYNOM7:def 1;

                

                 A36: g = g9 by A32, XTUPLE_0: 1;

                reconsider g9 as Polynomial of n, L by A34, POLYNOM1:def 11;

                reconsider h9 = h as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

                reconsider h9 as Element of ( Polynom-Ring (n,L));

                h reduces_to (g9,P,T) by A31, A36, Def13;

                then (h9,g) are_congruent_mod (P -Ideal ) by A36, Lm19;

                then (f,g) are_congruent_mod (P -Ideal ) by A30, Th54;

                hence (f - g) in (P -Ideal );

              end;

                case

                 A37: [g, h] in R;

                then

                consider g9,h9 be object such that

                 A38: [g, h] = [g9, h9] and

                 A39: g9 in ( NonZero ( Polynom-Ring (n,L))) and

                 A40: h9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

                

                 A41: g = g9 by A38, XTUPLE_0: 1;

                 not g9 in {( 0_ (n,L))} by A3, A39, XBOOLE_0:def 5;

                then

                 A42: g9 <> ( 0_ (n,L)) by TARSKI:def 1;

                

                 A43: h = h9 by A38, XTUPLE_0: 1;

                then

                reconsider h as Element of ( Polynom-Ring (n,L)) by A40;

                reconsider h9 as Polynomial of n, L by A43;

                reconsider g9 = g as non-zero Polynomial of n, L by A41, A42, POLYNOM1:def 11, POLYNOM7:def 1;

                reconsider gg = g9 as Element of ( Polynom-Ring (n,L));

                reconsider gg as Element of ( Polynom-Ring (n,L));

                reconsider h as Element of ( Polynom-Ring (n,L));

                g9 reduces_to (h9,P,T) by A37, A43, Def13;

                then (h,gg) are_congruent_mod (P -Ideal ) by A43, Lm19, Th53;

                then (f,gg) are_congruent_mod (P -Ideal ) by A30, Th54;

                hence (f - g) in (P -Ideal );

              end;

            end;

            hence (f,g) are_congruent_mod (P -Ideal );

          end;

          hence thesis;

        end;

      end;

      

       A44: P[1]

      proof

        let f,g be Element of ( Polynom-Ring (n,L));

        assume (R \/ (R ~ )) reduces (f,g);

        let p be RedSequence of (R \/ (R ~ ));

        assume (p . 1) = f & (p . ( len p)) = g & ( len p) = 1;

        then

         A45: (f - g) = ( 0. PR) by RLVECT_1: 15;

        ( 0. PR) in (P -Ideal ) by IDEAL_1: 3;

        hence thesis by A45;

      end;

      

       A46: for k be Nat st 1 <= k holds P[k] from NAT_1:sch 8( A44, A4);

      consider k be Nat such that

       A47: ( len p) = k;

      1 <= k by A47, NAT_1: 14;

      hence thesis by A46, A1, A2, A47;

    end;

    

     Lm20: for n be Nat, T be admissible connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L)), f,p,h be Element of ( Polynom-Ring (n,L)) st p in P & p <> ( 0_ (n,L)) & h <> ( 0_ (n,L)) holds (f,(f + (h * p))) are_convertible_wrt ( PolyRedRel (P,T))

    proof

      let n be Nat, T be admissible connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L)), f,p,h be Element of ( Polynom-Ring (n,L));

      assume that

       A1: p in P and

       A2: p <> ( 0_ (n,L)) and

       A3: h <> ( 0_ (n,L));

      set PR = ( Polynom-Ring (n,L));

      reconsider f9 = f, h9 = h, p9 = p as Element of PR;

      reconsider f9, p9, h9 as Polynomial of n, L by POLYNOM1:def 11;

      reconsider h9, p9 as non-zero Polynomial of n, L by A2, A3, POLYNOM7:def 1;

      

       A4: ( PolyRedRel (P,T)) reduces ((h9 *' p9),( 0_ (n,L))) by A1, Th45;

      now

        per cases ;

          case f9 = ( 0_ (n,L));

          then ( PolyRedRel (P,T)) reduces ((f9 + (h9 *' p9)),f9) by A4, Th2;

          then

           A5: (f9,(f9 + (h9 *' p9))) are_convertible_wrt ( PolyRedRel (P,T)) by REWRITE1: 25;

          (h9 *' p9) = (h * p) by POLYNOM1:def 11;

          hence thesis by A5, POLYNOM1:def 11;

        end;

          case f9 <> ( 0_ (n,L));

          then

          reconsider f9 as non-zero Polynomial of n, L by POLYNOM7:def 1;

          ((f9 + (h9 *' p9)) - f9) = ((f9 + (h9 *' p9)) + ( - f9)) by POLYNOM1:def 7

          .= ((h9 *' p9) + (f9 + ( - f9))) by POLYNOM1: 21

          .= (( 0_ (n,L)) + (h9 *' p9)) by Th3

          .= (h9 *' p9) by Th2;

          then

           A6: ( PolyRedRel (P,T)) reduces (((f9 + (h9 *' p9)) - f9),( 0_ (n,L))) by A1, Th45;

          now

            per cases ;

              case (f9 + (h9 *' p9)) <> ( 0_ (n,L));

              then

              reconsider g9 = (f9 + (h9 *' p9)) as non-zero Polynomial of n, L by POLYNOM7:def 1;

              (h9 *' p9) = (h * p) by POLYNOM1:def 11;

              then g9 = (f + (h * p)) by POLYNOM1:def 11;

              hence thesis by A6, Th51, REWRITE1: 31;

            end;

              case

               A7: (f9 + (h9 *' p9)) = ( 0_ (n,L));

              now

                assume

                 A8: ( - h9) = ( 0_ (n,L));

                 A9:

                now

                  let u be object;

                  assume u in ( dom h9);

                  then

                  reconsider u9 = u as bag of n;

                  ( - (h9 . u9)) = (( - h9) . u9) by POLYNOM1: 17

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

                  

                  then (h9 . u9) = ( - ( 0. L)) by RLVECT_1: 17

                  .= ( 0. L) by RLVECT_1: 12

                  .= (( 0_ (n,L)) . u9) by POLYNOM1: 22;

                  hence (h9 . u) = (( 0_ (n,L)) . u);

                end;

                ( dom h9) = ( Bags n) by FUNCT_2:def 1

                .= ( dom ( 0_ (n,L))) by FUNCT_2:def 1;

                hence contradiction by A3, A9, FUNCT_1: 2;

              end;

              then

              reconsider mh9 = ( - h9) as non-zero Polynomial of n, L by POLYNOM7:def 1;

              reconsider x = mh9 as Element of PR by POLYNOM1:def 11;

              reconsider x as Element of PR;

              (h + x) = (mh9 + h9) by POLYNOM1:def 11

              .= ( 0_ (n,L)) by Th3

              .= ( 0. PR) by POLYNOM1:def 11;

              then ( - h) = mh9 by RLVECT_1: 6;

              then

               A10: (( - h) * p) = (mh9 *' p9) by POLYNOM1:def 11;

              ( PolyRedRel (P,T)) reduces ((mh9 *' p9),( 0_ (n,L))) by A1, Th45;

              then

               A11: ((mh9 *' p9),( 0_ (n,L))) are_convertible_wrt ( PolyRedRel (P,T)) by REWRITE1: 25;

              (h9 *' p9) = (h * p) by POLYNOM1:def 11;

              

              then

               A12: (f + (h * p)) = ( 0_ (n,L)) by A7, POLYNOM1:def 11

              .= ( 0. PR) by POLYNOM1:def 11;

              

              then f = ( - (h * p)) by RLVECT_1: 6

              .= (( - h) * p) by VECTSP_1: 9;

              hence thesis by A12, A11, A10, POLYNOM1:def 11;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: POLYRED:58

    for n be Nat, T be admissible connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L)), f,g be Element of ( Polynom-Ring (n,L)) holds (f,g) are_congruent_mod (P -Ideal ) implies (f,g) are_convertible_wrt ( PolyRedRel (P,T))

    proof

      let n be Nat, T be admissible connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L)), f,g be Element of ( Polynom-Ring (n,L));

      set PR = ( Polynom-Ring (n,L));

      defpred P[ Nat] means for f,g be Element of ( Polynom-Ring (n,L)), p be LeftLinearCombination of P st ( Sum p) = (g - f) & ( len p) = $1 holds (f,g) are_convertible_wrt ( PolyRedRel (P,T));

      now

        let k be Nat;

        assume

         A1: P[k];

        now

          let f,g be Element of ( Polynom-Ring (n,L)), p be LeftLinearCombination of P;

          assume that

           A2: ( Sum p) = (g - f) and

           A3: ( len p) = (k + 1);

          now

            set h = (f + (p /. (k + 1)));

            set q = (p | ( Seg k));

            reconsider q as FinSequence by FINSEQ_1: 15;

            ( dom p) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

            then

            consider u be Element of PR, a be Element of P such that

             A4: (p /. (k + 1)) = (u * a) by FINSEQ_1: 4, IDEAL_1:def 9;

            reconsider u9 = u, a9 = a as Element of PR;

            reconsider u9, a9 as Polynomial of n, L by POLYNOM1:def 11;

            

             A5: (p /. (k + 1)) = (u9 *' a9) by A4, POLYNOM1:def 11;

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

            then

             A6: ( len q) = k by A3, FINSEQ_1: 17;

            reconsider q as LeftLinearCombination of P by IDEAL_1: 42;

            

             A7: ( Sum p) = (( Sum q) + (p /. (k + 1))) by A3, Lm6;

            

            then (( Sum p) - (p /. (k + 1))) = ((( Sum q) + (p /. (k + 1))) + ( - (p /. (k + 1))))

            .= (( Sum q) + ((p /. (k + 1)) + ( - (p /. (k + 1))))) by RLVECT_1:def 3

            .= (( Sum q) + ( 0. PR)) by RLVECT_1: 5

            .= ( Sum q) by RLVECT_1: 4;

            

            then ( Sum q) = ((g - f) + ( - (p /. (k + 1)))) by A2

            .= ((g + ( - f)) + ( - (p /. (k + 1))))

            .= (g + (( - f) + ( - (p /. (k + 1))))) by RLVECT_1:def 3

            .= (g + ( - h)) by RLVECT_1: 31

            .= (g - h);

            then

             A8: (h,g) are_convertible_wrt ( PolyRedRel (P,T)) by A1, A6;

            now

              per cases ;

                case a <> ( 0_ (n,L)) & u <> ( 0_ (n,L));

                then (f,h) are_convertible_wrt ( PolyRedRel (P,T)) by A4, Lm20;

                hence (f,g) are_convertible_wrt ( PolyRedRel (P,T)) by A8, REWRITE1: 30;

              end;

                case

                 A9: a = ( 0_ (n,L)) or u = ( 0_ (n,L));

                reconsider sumq = ( Sum q) as Polynomial of n, L by POLYNOM1:def 11;

                now

                  per cases by A9;

                    case a = ( 0_ (n,L));

                    hence (p /. (k + 1)) = ( 0_ (n,L)) by A5, POLYNOM1: 28;

                  end;

                    case u = ( 0_ (n,L));

                    hence (p /. (k + 1)) = ( 0_ (n,L)) by A5, Th5;

                  end;

                end;

                

                then ( Sum p) = (sumq + ( 0_ (n,L))) by A7, POLYNOM1:def 11

                .= ( Sum q) by POLYNOM1: 23;

                hence (f,g) are_convertible_wrt ( PolyRedRel (P,T)) by A1, A2, A6;

              end;

            end;

            hence (f,g) are_convertible_wrt ( PolyRedRel (P,T));

          end;

          hence (f,g) are_convertible_wrt ( PolyRedRel (P,T));

        end;

        hence P[(k + 1)];

      end;

      then

       A10: for k be Nat holds P[k] implies P[(k + 1)];

      

       A11: P[ 0 ]

      proof

        let f,g be Element of ( Polynom-Ring (n,L)), p be LeftLinearCombination of P;

        assume that

         A12: ( Sum p) = (g - f) and

         A13: ( len p) = 0 ;

        p = ( <*> the carrier of PR) by A13;

        then ( Sum p) = ( 0. PR) by RLVECT_1: 43;

        then f = g by A12, RLVECT_1: 21;

        hence thesis by REWRITE1: 26;

      end;

      

       A14: for k be Nat holds P[k] from NAT_1:sch 2( A11, A10);

      assume (f,g) are_congruent_mod (P -Ideal );

      then (g,f) are_congruent_mod (P -Ideal ) by Th53;

      then (g - f) in (P -Ideal );

      then (g - f) in (P -LeftIdeal ) by IDEAL_1: 63;

      then

      consider p be LeftLinearCombination of P such that

       A15: ( Sum p) = (g - f) by IDEAL_1: 61;

      ex k be Nat st ( len p) = k;

      hence thesis by A14, A15;

    end;

    theorem :: POLYRED:59

    

     Th59: for n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L holds ( PolyRedRel (P,T)) reduces (f,g) implies (f - g) in (P -Ideal )

    proof

      let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L;

      reconsider f9 = f, g9 = g as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider f9, g9 as Element of ( Polynom-Ring (n,L));

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

      reconsider x = ( - g) as Element of R by POLYNOM1:def 11;

      reconsider x as Element of R;

      (x + g9) = (( - g) + g) by POLYNOM1:def 11

      .= ( 0_ (n,L)) by Th3

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

      then

       A1: ( - g9) = ( - g) by RLVECT_1: 6;

      assume ( PolyRedRel (P,T)) reduces (f,g);

      then (f,g) are_convertible_wrt ( PolyRedRel (P,T)) by REWRITE1: 25;

      then

       A2: (f9,g9) are_congruent_mod (P -Ideal ) by Th57;

      (f - g) = (f + ( - g)) by POLYNOM1:def 7

      .= (f9 + ( - g9)) by A1, POLYNOM1:def 11

      .= (f9 - g9);

      hence thesis by A2;

    end;

    theorem :: POLYRED:60

    for n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f be Polynomial of n, L holds ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L))) implies f in (P -Ideal )

    proof

      let n be Ordinal, T be connected TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f be Polynomial of n, L;

      assume ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L)));

      then (f - ( 0_ (n,L))) in (P -Ideal ) by Th59;

      hence thesis by Th4;

    end;