POLYRED

:: Polynomial Reduction
::  by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ORDINAL1, ZFMISC_1, STRUCT_0, VALUED_0, POLYNOM7,
      SUBSET_1, RELAT_1, SUPINF_2, POLYNOM1, VECTSP_1, ORDERS_1, TARSKI,
      PRE_POLY, ARYTM_3, FUNCT_1, ALGSEQ_1, NAT_1, FINSET_1, CARD_1, XXREAL_0,
      XBOOLE_0, RLVECT_1, ALGSTR_0, FINSEQ_1, CARD_3, PARTFUN1, ORDINAL4,
      ARYTM_1, ALGSTR_1, LATTICES, VECTSP_2, BINOP_1, CAT_3, RELAT_2, BAGORDER,
      TERMORD, XCMPLX_0, BROUWER, ORDERS_2, WELLORD1, FINSUB_1, WAYBEL_4,
      MESFUNC1, REWRITE1, INT_1, IDEAL_1, POLYRED;
 notations CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1,
      ZFMISC_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FINSET_1, XXREAL_0, STRUCT_0, ALGSTR_0, ALGSTR_1, WAYBEL_0, FINSUB_1,
      WAYBEL_4, REWRITE1, RLVECT_1, FINSEQ_1, XTUPLE_0, MCART_1, ORDERS_1,
      VFUNCT_1, GROUP_1, VECTSP_2, VECTSP_1, POLYNOM7, WELLORD1, WELLFND1,
      IDEAL_1, ORDERS_2, POLYNOM1, BAGORDER, TERMORD, PRE_POLY;
 constructors REWRITE1, VECTSP_2, TRIANG_1, WAYBEL_4, WELLFND1, IDEAL_1,
      BAGORDER, TERMORD, DOMAIN_1, RELSET_1, BINOP_2, FVSUM_1, VFUNCT_1,
      XTUPLE_0;
 registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, FINSUB_1, XREAL_0, NAT_1,
      CARD_1, FINSEQ_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1,
      GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, BAGORDER,
      TERMORD, VALUED_0, ALGSTR_0, PRE_POLY, VFUNCT_1, FUNCT_2, FUNCT_1,
      RELSET_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE;
 definitions POLYNOM7;
 equalities STRUCT_0, POLYNOM7, ALGSTR_0;
 expansions STRUCT_0, POLYNOM7;
 theorems TARSKI, RELSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, ZFMISC_1,
      VECTSP_1, POLYNOM1, BINOM, RLVECT_1, VECTSP_2, FINSET_1, NAT_1, POLYNOM2,
      ALGSTR_1, RELAT_2, CARD_1, CARD_2, WAYBEL_0, ORDERS_2, ORDERS_1,
      POLYNOM7, FINSUB_1, WELLORD1, WELLFND1, REWRITE1, WAYBEL_4, XBOOLE_0,
      XBOOLE_1, MATRLIN, IDEAL_1, BAGORDER, TERMORD, XCMPLX_1, GROUP_1,
      XREAL_1, XXREAL_0, PARTFUN1, STRUCT_0, PRE_POLY, XTUPLE_0;
 schemes NAT_1, RELSET_1;

begin :: Preliminaries

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 being set, S being Subset of X, R being 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,38;
end;

Lm2: for n being Ordinal, b1,b2,b3 being 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 being Ordinal such that
A2: b1.k < b2.k and
A3: for l being 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 being Ordinal, b1,b2 being 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 being Ordinal, b1,b2 being 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 being Ordinal st b1.k < b2.k & for l being 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 being Ordinal, L being non trivial ZeroStr, p being non-zero
finite-Support Series of n,L holds ex b being bag of n st p.b <> 0.L & for b9
being 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 being finite Subset of Bags n st card B = $1
holds ex b being bag of n st b in B & for b9 being bag of n st b9 in B holds b9
  <=' b;
A1: for k being 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 being bag of n such that
A7:     b in X and
A8:     for b9 being 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 being 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 being 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 being 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 being 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 being bag of n st b9 in B holds b9 <=' b by A19,TARSKI:def 1;
    hence thesis by A20;
  end;
  for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A18,A1);
  then consider b being bag of n such that
A21: b in Support p and
A22: for b9 being 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 being Abelian add-associative right_zeroed right_complementable
non empty addLoopStr, f,g being FinSequence of the carrier of L, n being 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 is Nat : 1 <= k & k <= n+1 } by A5,FINSEQ_1:def 1;
    then consider i being 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
          .= 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 is 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 being bag of n such that
A1: q.b22 <> 0.L and
A2: for b9 being bag of n st b22 < b9 holds q.b9 = 0.L by Lm5;
    consider b11 being bag of n such that
A3: p.b11 <> 0.L and
A4: for b9 being bag of n st b11 < b9 holds p.b9 = 0.L by Lm5;
    set b = b11 + b22;
    consider s being 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 being Element of NAT st k in dom s ex b1, b2 being 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 being non empty finite Subset of Bags n such that
A9: divisors b = SgmX(BagOrder n, S) and
A10: for p being 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 being 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 being 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;
A22: now
      let k be Element of NAT;
      assume that
A23:  k in dom s and
A24:  k <> i;
      consider b1,b2 being 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 being 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;
A30:  b1 = <*b19, b29*>.1 by A27,A25,FINSEQ_1:44
        .= b19;
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;
    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 :: More on Polynomials and Monomials

theorem Th1:
  for X being set, L being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, p,q being 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 Th2:
  for X being set, L being left_zeroed non empty addLoopStr, p
  being 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 Th3:
  for X being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p being 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 Th4:
  for n being set, L being 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 Th5:
  for n being Ordinal, L being add-associative right_complementable
right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr, p
  being 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 being FinSequence of the carrier of L such that
A1: (Z*'p).b = Sum s and
    len s = len decomp b and
A2: for k being Element of NAT st k in dom s ex b1, b2 being 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 being 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 being Ordinal, L being Abelian right_zeroed add-associative
right_complementable well-unital distributive associative commutative non
trivial doubleLoopStr, p being Polynomial of n,L, q being 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 Th6:
  for n being Ordinal, L being Abelian right_zeroed add-associative
  right_complementable well-unital distributive associative commutative non
trivial doubleLoopStr, p,q being 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 being Ordinal, L being add-associative right_complementable
right_zeroed non empty addLoopStr, p being Polynomial of n,L, m being
Monomial of n,L, b being 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 Th7:
  for n being Ordinal, L being add-associative right_complementable
right_zeroed distributive non empty doubleLoopStr, p being Polynomial of n,L,
m being Monomial of n,L, b being 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 being FinSequence of the carrier of L such that
A1: q.b = Sum s and
A2: len s = len decomp b and
A3: for k being Element of NAT st k in dom s ex b1,b2 being bag of n st
  (decomp b)/.k = <*b1, b2*> & s/.k = m.b1*p.b2 by POLYNOM1:def 10;
  consider k being 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 being 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
    .= b29 by A5,A7,FINSEQ_1:44;
A10: for k9 being 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 being 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
      .= <*b19,b29*>.2 by A6,A11,A13,A15,PRE_POLY:def 17
      .= b29;
    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
    .= b19;
  hence thesis by A1,A6,A4,A8,A9,A10,POLYNOM2:3;
end;

theorem Th8:
  for X being set, L being right_zeroed left_add-cancelable
left-distributive non empty doubleLoopStr, p being 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 Th9:
  for X being set, L being add-associative right_zeroed
right_complementable distributive non empty doubleLoopStr, p being Series of
  X,L, a being 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 Th10:
  for X being set, L being left-distributive non empty
  doubleLoopStr, p being Series of X,L, a,a9 being 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 Th11:
  for X being set, L being associative non empty multLoopStr_0,
p being Series of X,L, a,a9 being 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 Th12:
  for n being Ordinal, L being add-associative right_zeroed
  right_complementable well-unital associative commutative distributive non
empty doubleLoopStr, p,p9 being Series of n,L, a being 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 being FinSequence of the carrier of L such that
A2: pap.b = Sum s and
A3: len s = len decomp b and
A4: for k being Element of NAT st k in dom s ex b1,b2 being bag of n
    st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*(a*p9).b2 by POLYNOM1:def 10;
    consider t being FinSequence of the carrier of L such that
A5: pp.b = Sum t and
A6: len t = len decomp b and
A7: for k being Element of NAT st k in dom t ex b1,b2 being 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 being 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 being 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
        .= a2;
      b1 = <*a1,a2*>.1 by A10,A12
        .= a1;
      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 :: Multiplication of polynomials with bags

definition
  let n be Ordinal, b be bag of n, L be non empty ZeroStr, p be Series of n,L;
  func b *' p -> Series of n,L means
  :Def1:
  for b9 being bag of n st b divides
b9 holds it.b9 = p.(b9 -' b) & for b9 being bag of n st not b divides b9 holds
  it.b9 = 0.L;
  existence
  proof
    set M1 = {[b9,p.(b9-'b)] where b9 is Element of Bags n : b divides b9}, M2
    = {[b9,0.L] where b9 is 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 being 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 being 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 is 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 is 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 being 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 being Element of Bags n such that
A10:    [v,0.L] = [x,y1] and
A11:    not b divides v by A8;
        consider u being 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 being Element of Bags n such that
A17:    [v,0.L] = [x,y2] and
A18:    not b divides v by A16;
        consider u being 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 being Element of Bags n such that
A24:      [v,p.(v-'b)] = [x,y2] and
          b divides v;
          consider u being 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 being Element of Bags n st [v,0.L] = [x,y2] & not b divides v;
A28:      ex u being 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 is 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 is 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 being bag of n st b divides b9 holds p1.b9 = p.(b9 -' b) &
    for b9 being bag of n st not b divides b9 holds p1.b9 = 0.L and
A33: for b9 being bag of n st b divides b9 holds p2.b9 = p.(b9 -' b) &
    for b9 being 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 being Ordinal, b,b9 being bag of n, L being non empty ZeroStr, p
being 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 being Ordinal, L being non empty ZeroStr, p being Polynomial of n,
L, b being bag of n holds Support(b*'p) c= {b + b9 where b9 is 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 being 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 is 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 is Element of Bags n : b9 in Support p};
A1: now
      let u be object;
      assume u in f;
      then ex b9 being Element of Bags n st u = [b9,b+b9] & b9 in Support p;
      hence ex y,z being 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 being Element of Bags n such that
A4:   [x,y2] = [b2,b+b2] and
      b2 in Support p by A3;
      consider b1 being 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 being object such that
A7:   [u,v] in f by XTUPLE_0:def 12;
      consider b9 being 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 is 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 is Element of Bags n : b9 in Support p} by A10;
      then consider b9 being 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 is 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
  for n being Ordinal, b,b9 being bag of n, L being non empty ZeroStr, p
  being Series of n,L holds (b*'p).(b9+b) = p.b9 by Lm9;

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

theorem Th15:
  for n being Ordinal, T being connected admissible TermOrder of n
, L being non trivial ZeroStr, p being non-zero Polynomial of n,L, b being 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 being 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 Th16:
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being non empty ZeroStr, p being Polynomial of n,L, b,b9 being 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 is Element of Bags n : b2 in Support p
  } by Lm10;
  then b9 in {b + b2 where b2 is Element of Bags n : b2 in Support p} by A1;
  then consider s being 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
  for n being Ordinal, T being connected TermOrder of n, L being non
  empty ZeroStr, p being 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 Th18:
  for n being Ordinal, T being connected TermOrder of n, L being
non empty ZeroStr, p being Series of n,L, b1,b2 being 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 being 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 Th19:
  for n being Ordinal, L being add-associative right_zeroed
  right_complementable distributive non trivial doubleLoopStr, p being
  Polynomial of n,L, a being 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 being 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
  for n being Ordinal, L being domRing-like non trivial doubleLoopStr,
  p being Polynomial of n,L, a being 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 Th21:
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_zeroed right_complementable distributive domRing-like
non trivial doubleLoopStr, p being Polynomial of n,L, a being 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 Th22:
  for n being Ordinal, L being add-associative
  right_complementable right_zeroed distributive non trivial doubleLoopStr, p
being Series of n,L, b being bag of n, a being 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 being FinSequence of the carrier of L such that
A2:   q9.s = Sum t and
A3:   len t = len decomp s and
A4:   for k being Element of NAT st k in dom t ex b1, b2 being 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 being bag of n such that
A9:       b + s9 = s by A7,TERMORD:1;
          consider i being 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 being 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;
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 being 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 being 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;
            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;
          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 being FinSequence of the carrier of L such that
A26:      q9.s = Sum t and
A27:      len t = len decomp s and
A28:      for k being Element of NAT st k in dom t ex b1, b2 being
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 being 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 being 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;
                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
  for n being Ordinal, T being connected admissible TermOrder of n, L
  being add-associative right_complementable right_zeroed well-unital
  distributive domRing-like non trivial doubleLoopStr, p being non-zero
Polynomial of n,L, q being Polynomial of n,L, m being 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 :: Orders on Polynomials

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 being 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 being Ordinal, T being connected TermOrder of n, L being non empty
ZeroStr, p being 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 :: according to p. 193
  let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p,q
  be Polynomial of n,L;
  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;
  pred p < q,T means

  p <= q,T & Support p <> Support q;
end;

definition
  let n being Ordinal, T being connected TermOrder of n, L being non empty
  ZeroStr, p being Polynomial of n,L;
  func Support(p,T) -> Element of Fin the carrier of RelStr(#Bags n,T#) equals
  Support(p);
  coherence by Lm11;
end;

theorem Th24: :: according to definition 5.15, p. 194
  for n being Ordinal, T being connected TermOrder of n, L being
non trivial ZeroStr, p being 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 being set st y in sp & y <> htp & [htp,y] in the InternalRel of R;
    then consider y being 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,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 Th25:

:: theorem 5.12, p. 193
  for n being Ordinal, T being connected TermOrder of n, L being
  non empty addLoopStr, p being Polynomial of n,L holds p <= p,T
by Lm11,ORDERS_1:3;

Lm12: for n being Ordinal, T being connected TermOrder of n, L being non empty
ZeroStr, p being 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 is 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 Th26:

:: theorem 5.12, p. 193
  for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q being 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 being 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 Th27:

:: theorem 5.12, p. 193
  for n being Ordinal, T being connected TermOrder of n, L being
  non empty addLoopStr, p,q,r being 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 Th28:
  for n being Ordinal, T being connected TermOrder of n, L being
  non empty addLoopStr, p,q being 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 Th29:
  for n being Ordinal, T being connected TermOrder of n, L being
non empty addLoopStr, p,q being 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 being 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 being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, p
being Polynomial of n,L, b being 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 being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed non trivial addLoopStr
, p being 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 being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed non trivial addLoopStr
, p,q being 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 being 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 being 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
  for n being Ordinal, T being connected TermOrder of n, L being non
  empty ZeroStr, p being Polynomial of n,L holds 0_(n,L) <= p,T by Lm12;

Lm16: for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed non trivial addLoopStr
, p,q being 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 Th31:

:: according to p. 193
  for n being Nat, T being admissible connected TermOrder of n, L
  being add-associative right_complementable right_zeroed well-unital
  distributive non trivial doubleLoopStr, P being non empty Subset of
  Polynom-Ring(n,L) holds ex p being Polynomial of n,L st p in P & for q being
  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 is 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 being 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 being 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
  for n being Ordinal, T being connected admissible TermOrder of n, L
being add-associative right_complementable right_zeroed non trivial addLoopStr
, p,q being 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 Th33: :: exercise 5.16, p. 194
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed non trivial
  addLoopStr, p being 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 is 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 Th34: :: exercise 5.16, p. 194
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed non trivial addLoopStr, p
  being 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 being 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 Th35:
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed non trivial
  addLoopStr, p being 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 :: Polynomial Reduction

definition :: definition 5.18 (i), p. 195
  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;
  pred f reduces_to g,p,b,T means

  f <> 0_(n,L) & p <> 0_(n,L) & b in
Support f & ex s being bag of n st s + HT(p,T) = b & g = f - (f.b/HC(p,T)) * (s
  *' p);
end;

definition :: definition 5.18 (ii), p. 195
  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;
  pred f reduces_to g,p,T means

  ex b being bag of n st f reduces_to g,p ,b,T;
end;

definition :: definition 5.18 (iii), p. 196
  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);
  pred f reduces_to g,P,T means

  ex p being Polynomial of n,L st p in P & f reduces_to g,p,T;
end;

definition :: definition 5.18 (iv), p. 196
  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;
  pred f is_reducible_wrt p,T means

  ex g being Polynomial of n,L st f reduces_to g,p,T;
end;

notation :: definition 5.18 (iv), p. 196
  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 :: definition 5.18 (v), p. 196
  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);
  pred f is_reducible_wrt P,T means
  ex g being Polynomial of n,L st f reduces_to g,P,T;
end;

notation :: definition 5.18 (v), p. 196
  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 :: following definition 5.18, p. 196
  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;
  pred f top_reduces_to g,p,T means
  f reduces_to g,p,HT(f,T),T;
end;

definition :: following definition 5.18, p. 196
  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;
  pred f is_top_reducible_wrt p,T means
  ex g being Polynomial of n,L st f top_reduces_to g,p,T;
end;

definition :: following definition 5.18, p. 196
  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);
  pred f is_top_reducible_wrt P,T means
  ex p being Polynomial of n,L st p in P & f is_top_reducible_wrt p,T;
end;

theorem :: lemma 5.20 (i), p. 197
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f
  being Polynomial of n,L, p being non-zero Polynomial of n,L holds f
  is_reducible_wrt p,T iff ex b being 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 being bag of n st b in Support f & HT(p,T) divides b;
    then consider b being bag of n such that
A3: b in Support f and
A4: HT(p,T) divides b;
    consider s being 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 being Polynomial of n,L such that
A6: f reduces_to g,p,T;
    consider b being bag of n such that
A7: f reduces_to g,p,b,T by A6;
    ex s being 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 being bag of n st b in Support f & HT(p,T) divides b by A8;
  end;
  hence thesis by A1;
end;

Lm17: for n being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,
p,g being Polynomial of n,L, b being 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 being bag of n st s + HT(p,T) = b & g = f - (f.b)/
  HC(p,T) * (s *' p );
  then consider s being 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 Th37:
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, p
  being 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 being Polynomial of n,L such that
A1: 0_(n,L) reduces_to g,p,T;
  ex b being bag of n st 0_(n,L) reduces_to g,p,b,T by A1;
  hence thesis;
end;

theorem :: lemma 5.20 (ii), p. 197
  for n being Ordinal, T being admissible connected TermOrder of n, L
being add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non degenerated non
empty doubleLoopStr, f,p being Polynomial of n,L, m being 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 being 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 being 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 :: lemma 5.20 (iii), p. 197
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive almost_left_invertible non degenerated non empty
  doubleLoopStr, f,p,g being Polynomial of n,L, b being bag of n holds f
  reduces_to g,p,b,T implies not(b in Support g) by Lm17;

theorem Th40: :: lemma 5.20 (iii), p. 197
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being 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 being 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 Th41:
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, f,p,g being Polynomial of n,L, b,b9 being 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 being 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 Th42:
  for n being Ordinal, T being connected admissible TermOrder of n
  , L being add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, f,p,g being Polynomial of n,L holds f reduces_to g,p,
  T implies for b being 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 being 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 Th43: :: lemma 5.20 (iv), p. 197
  for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, f,p,g being 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 being 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 being Nat st card(Support f) = k;
  assume
A2: f reduces_to g,p,T;
  then consider b being 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 being 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 being bag of n such that
A9:   f reduces_to g,p,b,T by A8;
      consider s being 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 being 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 being 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 :: Polynomial Reduction Relation

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);
  func PolyRedRel(P,T) -> Relation of NonZero Polynom-Ring(n,L), the carrier
  of Polynom-Ring(n,L) means
  :Def13:
  for p,q being 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 being 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 being Relation of A,B such that
A1: for x,y being 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 being Polynomial of n,L such that
        pp in P and
A4:     p reduces_to q,pp,T;
        ex b being 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 being Polynomial of n,L holds [p,q] in R1 iff p
    reduces_to q,P,T and
A8: for p,q being Polynomial of n,L holds [p,q] in R2 iff p reduces_to q,P,T;
    for p,q being 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 being 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 being 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 being Ordinal, T being connected TermOrder of n, L being
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, f,
g,p being 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 being bag of n st f reduces_to g,p,b,T;
  hence thesis;
end;

theorem :: lemma 5.20 (v), p. 197
  for n being Ordinal, T being connected admissible TermOrder of n, L
  being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, f,g being Polynomial of n,L, P being 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 being Polynomial of n,L st PolyRedRel(P,T)
reduces f,g for p being 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 being 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 being 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 being 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 being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A29,A3);
  consider k being 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 :: theorem 5.21, p. 198
  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 is Polynomial of n,L : ex y being 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 being Polynomial of n,L st Support p = u & ex y being 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 being object such that
A7:   a in M and
A8:   X-Seg a misses M by A2,WELLORD1:def 3;
      consider p being Polynomial of n,L such that
A9:   Support p = a and
A10:  ex y being 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 being 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 being 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 being 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 being 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 being 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 Th45: :: lemma 5.24 (i), p. 200
  for n being Nat, T being admissible connected TermOrder of n, L
being add-associative right_complementable left_zeroed right_zeroed commutative
  associative well-unital distributive Abelian almost_left_invertible non
  trivial doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,h being
  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 is 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 being 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 being Polynomial of n,L such that
A3:       m in H and
A4:       for m9 being 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 being 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 being 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 Th46: :: lemma 5.24 (ii), p. 200
  for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being
  Polynomial of n,L, m being 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 being Polynomial of n,L such that
A1: p in P and
A2: f reduces_to g,p,T;
  consider b being 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 being 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 Th47: :: lemma 5.24 (iii), p. 200
  for n being Ordinal, T being connected admissible TermOrder of n
, L being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being
  Polynomial of n,L, m being 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 being Polynomial of n,L st PolyRedRel(P,T)
reduces f,g for p being 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 being RedSequence of R such that
A3: p.1 = f & p.len p = g by A1,REWRITE1:def 3;
    consider k being 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 being 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 being 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 :: lemma 5.24 (iii), p. 200
  for n being Ordinal, T being connected admissible TermOrder of n, L
  being Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being Subset of Polynom-Ring(n,L), f being
Polynomial of n,L, m being 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 Th49: :: lemma 5.25 (i), p. 200
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g,h,h1 being Polynomial
of n,L holds (f - g = h & PolyRedRel(P,T) reduces h,h1) implies ex f1,g1 being
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 being 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 being Polynomial of n,L st f - g = h for h1
being Polynomial of n,L for p being RedSequence of PolyRedRel(P,T) st p.1 = h &
  p.len p = h1 & len p = $1 holds ex f1,g1 being 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 being 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 being Polynomial of n,L such that
A17:  p in P and
A18:  h2 reduces_to h1,p,T;
      consider b being 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 being 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 being 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 being 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 being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A46,A4);
  consider k being Nat such that
A50: len p = k;
  1 <= k by A50,NAT_1:14;
  hence thesis by A1,A49,A3,A50;
end;

theorem Th50: :: lemma 5.25 (ii), p. 200
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being 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 being 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 Th51: :: lemma 5.25 (ii), p. 200
  for n being Ordinal, T being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed commutative associative
  well-unital distributive Abelian almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being 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 being 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;
  pred a,b are_congruent_mod I means

  a - b in I;
end;

theorem
  for R being add-associative left_zeroed right_zeroed
  right_complementable right-distributive non empty doubleLoopStr, I being
  right-ideal non empty Subset of R, a being 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 Th53:
  for R being add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr, I being right-ideal
  non empty Subset of R, a,b being 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 Th54:
  for R being add-associative right_zeroed right_complementable
non empty addLoopStr, I being add-closed non empty Subset of R, a,b,c being
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
  for R being Abelian add-associative right_zeroed right_complementable
  well-unital distributive associative non trivial doubleLoopStr, I being
  add-closed non empty Subset of R, a,b,c,d being 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
  for R being add-associative right_zeroed right_complementable
  commutative distributive non empty doubleLoopStr, I being add-closed
  right-ideal non empty Subset of R, a,b,c,d being 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 being Ordinal, T being connected TermOrder of n, L being Abelian
add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, P
being Subset of Polynom-Ring(n,L), f being non-zero Polynomial of n,L, g being
Polynomial of n,L, f9,g9 being 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 being Polynomial of n,L such that
A4: p in P and
A5: f reduces_to g,p,T;
  consider b being bag of n such that
A6: f reduces_to g,p,b,T by A5;
  consider s being 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;
    hence
    ex u,v being Element of R, a being 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 Th57: :: lemma 5.26, p. 202
  for n being Ordinal, T being connected TermOrder of n, L being
  Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
  doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being 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 being Element of Polynom-Ring(n,L) st R \/ R~
reduces f,g for p being 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 being 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 being 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 being 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 being 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 being 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 being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A44,A4);
  consider k being 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 being Nat, T being admissible connected TermOrder of n, L being
Abelian add-associative right_complementable right_zeroed commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L), f,p,h
being 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 :: lemma 5.26, p. 202
  for n being Nat, T being admissible connected TermOrder of n, L being
  Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non degenerated
  non empty doubleLoopStr, P being non empty Subset of Polynom-Ring(n,L), f,g
being 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 being Element of Polynom-Ring(n,L), p being
  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 being Element of PR,a being 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 being 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 being 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 being LeftLinearCombination of P such that
A15: Sum p = g - f by IDEAL_1:61;
  ex k being Nat st len p = k;
  hence thesis by A14,A15;
end;

theorem Th59: :: lemma 5.26, p. 202
  for n being Ordinal, T being connected TermOrder of n, L being
  Abelian add-associative right_complementable right_zeroed commutative
  associative well-unital distributive almost_left_invertible non trivial
doubleLoopStr, P being Subset of Polynom-Ring(n,L), f,g being 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 :: lemma 5.26, p. 202
  for n being Ordinal, T being connected TermOrder of n, L being Abelian
  add-associative right_complementable right_zeroed commutative associative
well-unital distributive almost_left_invertible non trivial doubleLoopStr, P
being Subset of Polynom-Ring(n,L), f being 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;