:: Term Orders
::  by Christoph Schwarzweller
::
:: Received December 20, 2002
:: Copyright (c) 2002-2012 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, ZFMISC_1, ALGSTR_0, VECTSP_1, RLVECT_1, PRE_POLY,
      XCMPLX_0, ARYTM_3, FUNCT_1, XXREAL_0, ARYTM_1, CARD_1, XBOOLE_0,
      SUBSET_1, MCART_1, RELAT_1, PBOOLE, TARSKI, ORDINAL1, LATTICES, POLYNOM1,
      FINSEQ_1, CARD_3, PARTFUN1, NAT_1, SUPINF_2, POLYNOM7, STRUCT_0,
      VECTSP_2, CAT_3, BAGORDER, RELAT_2, WELLORD1, FINSET_1, BROUWER,
      VALUED_0, ORDERS_1, ALGSTR_1, TERMORD;
 notations NUMBERS, XCMPLX_0, TARSKI, XBOOLE_0, SUBSET_1, ORDERS_1, RELAT_1,
      CARD_1, BAGORDER, RELSET_1, FUNCT_1, PARTFUN1, FINSET_1, XXREAL_0,
      ORDINAL1, ALGSTR_1, PBOOLE, FINSEQ_1, PRE_POLY, STRUCT_0, ALGSTR_0,
      RLVECT_1, VFUNCT_1, XTUPLE_0, MCART_1, VECTSP_1, VECTSP_2, RELAT_2,
      POLYNOM1, NAT_D, WELLORD1, POLYNOM7;
 constructors VECTSP_2, ALGSTR_1, TRIANG_1, POLYNOM7, BAGORDER, WELLORD2,
      RELSET_1, POLYNOM1, BINOP_2, VFUNCT_1, XTUPLE_0;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0,
      NAT_1, CARD_1, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM1,
      POLYNOM2, POLYNOM7, BAGORDER, VALUED_0, PRE_POLY, VFUNCT_1, FUNCT_2,
      FUNCT_1, XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions XTUPLE_0;
 theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, POLYNOM1, NAT_1, BINOM,
      RLVECT_1, VECTSP_2, POLYNOM7, POLYNOM2, NAT_2, RELAT_2, CARD_1, CARD_2,
      MATRLIN, XBOOLE_0, XBOOLE_1, ORDERS_1, MCART_1, BAGORDER, WELLORD1,
      VECTSP_1, XREAL_1, PARTFUN1, VALUED_0, STRUCT_0, XREAL_0, PRE_POLY,
      XTUPLE_0;
 schemes NAT_1;

begin :: Preliminaries

registration
  cluster non trivial for addLoopStr;
  existence
  proof
    take  the Field;
    thus thesis;
  end;
end;

registration
  cluster add-associative right_complementable right_zeroed for non trivial
    addLoopStr;
  existence
  proof
    set F = the Field;
    take F;
    thus thesis;
  end;
end;

definition
  let X be set, b be bag of X;
  attr b is zero means
  b = EmptyBag X;
end;

theorem Th1:
  for X being set, b1,b2 being bag of X holds b1 divides b2 iff ex
  b being bag of X st b2 = b1 + b
proof
  let n be set, b1,b2 be bag of n;
  now
    assume
A1: b1 divides b2;
A2: now
      let k be set;
      b1.k <= b2.k by A1,PRE_POLY:def 11;
      then b1.k - b1.k <= b2.k - b1.k by XREAL_1:9;
      hence 0 <= b2.k - b1.k;
    end;
    now
      per cases;
      case
A3:     n = {};
        then b1 + EmptyBag n = EmptyBag n by POLYNOM7:3
          .= b2 by A3,POLYNOM7:3;
        hence ex b being bag of n st b2 = b1 + b;
      end;
      case
        n <> {};
        then reconsider n9 = n as non empty set;
        set b = { [k,b2.k -' b1.k] where k is Element of n9 : not
        contradiction};
A4:     now
          let x be set;
          assume x in b;
          then ex k being Element of n9 st x = [k,b2.k -' b1.k];
          hence ex y,z being set st x = [y,z];
        end;
        now
          let x,y1,y2 be set;
          assume that
A5:       [x,y1] in b and
A6:       [x,y2] in b;
          consider k being Element of n9 such that
A7:       [x,y1] = [k,b2.k -' b1.k] by A5;
          consider k9 being Element of n9 such that
A8:       [x,y2] = [k9,b2.k9 -' b1.k9] by A6;
          k = x by A7,XTUPLE_0:1
            .= k9 by A8,XTUPLE_0:1;
          hence y1 = y2 by A7,A8,XTUPLE_0:1;
        end;
        then reconsider b as Function by A4,FUNCT_1:def 1,RELAT_1:def 1;
A9:     now
          let x be set;
          assume x in dom b;
          then consider y being set such that
A10:      [x,y] in b by XTUPLE_0:def 12;
          consider k being Element of n9 such that
A11:      [x,y] = [k,b2.k -' b1.k] by A10;
          x = k by A11,XTUPLE_0:1;
          hence x in n9;
        end;
        now
          let x be set;
          assume x in n9;
          then reconsider k = x as Element of n9;
          [k,b2.k -' b1.k] in b;
          hence x in dom b by XTUPLE_0:def 12;
        end;
        then
A12:    dom b = n9 by A9,TARSKI:1;
        then reconsider b as ManySortedSet of n9 by PARTFUN1:def 2
,RELAT_1:def 18;
A13:    now
          let k be set;
          assume k in n;
          then consider u being set such that
A14:      [k,u] in b by A12,XTUPLE_0:def 12;
          consider k9 being Element of n9 such that
A15:      [k,u] = [k9,b2.k9 -' b1.k9] by A14;
A16:      u = b2.k9 -' b1.k9 by A15,XTUPLE_0:1;
          k = k9 by A15,XTUPLE_0:1;
          hence b.k = b2.k -' b1.k by A14,A16,FUNCT_1:1;
        end;
        now
          let x be set;
A17:      support b c= dom b by PRE_POLY:37;
          assume
A18:      x in support b;
          then
A19:      b.x <> 0 by PRE_POLY:def 7;
          now
            assume not x in support b2;
            then b2.x = 0 by PRE_POLY:def 7;
            then 0 = b2.x-'b1.x by NAT_2:8;
            hence contradiction by A12,A13,A18,A19,A17;
          end;
          hence x in support b2;
        end;
        then
A20:    support b c= support b2 by TARSKI:def 3;
        now
          let x be set;
          assume x in rng b;
          then consider y be set such that
A21:      [y,x] in b by XTUPLE_0:def 13;
          consider k being Element of n9 such that
A22:      [y,x] = [k,b2.k -' b1.k] by A21;
          x = b2.k -' b1.k by A22,XTUPLE_0:1;
          hence x in NAT;
        end;
        then rng b c= NAT by TARSKI:def 3;
        then reconsider b as bag of n by A20,PRE_POLY:def 8,VALUED_0:def 6;
        take b;
        now
          let k be set;
A23:      0 <= b2.k - b1.k by A2;
          assume k in n;
          hence b1.k + b.k = b1.k + (b2.k -' b1.k) by A13
            .= b1.k + (b2.k + -b1.k) by A23,XREAL_0:def 2
            .= b2.k;
        end;
        then b2 = b1 + b by PRE_POLY:33;
        hence ex b being bag of n st b2 = b1 + b;
      end;
    end;
    hence ex b being bag of n st b2 = b1 + b;
  end;
  hence thesis by PRE_POLY:50;
end;

theorem Th2:
  for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital 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
  well-unital 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 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 9;
    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 by VECTSP_1:7;
    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;

registration
  let n be Ordinal, L be add-associative right_complementable right_zeroed
  well-unital distributive non empty doubleLoopStr, m1,m2 be Monomial of n,L;
  cluster m1 *' m2 -> monomial-like;
  coherence
  proof
    per cases;
    suppose
      Support(m1*'m2) = {};
      hence thesis by POLYNOM7:6;
    end;
    suppose
A1:   Support(m1*'m2) <> {};
      now
        per cases;
        case
A2:       Support(m1) <> {} & Support(m2) <> {};
          then consider mb2 being bag of n such that
A3:       Support(m2) = {mb2} by POLYNOM7:6;
          mb2 in Support m2 by A3,TARSKI:def 1;
          then
A4:       m2.mb2 <> 0.L by POLYNOM1:def 3;
A5:       now
            let b be bag of n;
            assume
A6:         b <> mb2;
            consider b9 being bag of n such that
A7:         for b being bag of n st b <> b9 holds m2.b = 0.L by POLYNOM7:def 3;
            b9 = mb2 by A4,A7;
            hence m2.b = 0.L by A6,A7;
          end;
          consider mb1 being bag of n such that
A8:       Support(m1) = {mb1} by A2,POLYNOM7:6;
          mb1 in Support m1 by A8,TARSKI:def 1;
          then
A9:       m1.mb1 <> 0.L by POLYNOM1:def 3;
A10:      now
            let b be bag of n;
            assume
A11:        b <> mb1;
            consider b9 being bag of n such that
A12:        for b being bag of n st b <> b9 holds m1.b = 0.L by POLYNOM7:def 3;
            b9 = mb1 by A9,A12;
            hence m1.b = 0.L by A11,A12;
          end;
          set b = the Element of Support(m1*'m2);
A13:      b in Support(m1*'m2) by A1;
          then b is Element of Bags n;
          then reconsider b as bag of n;
          consider s being FinSequence of L such that
A14:      (m1*'m2).b = Sum s and
A15:      len s = len decomp b and
A16:      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 = m1.b1*m2.b2 by POLYNOM1:def 9;
A17:      dom s = Seg(len decomp b) by A15,FINSEQ_1:def 3
            .= dom(decomp b) by FINSEQ_1:def 3;
A18:      now
            assume
A19:        b <> mb1 + mb2;
A20:        now
              let k be Element of NAT;
              assume
A21:          k in dom s;
              then consider b1,b2 being bag of n such that
A22:          (decomp b)/.k = <*b1, b2*> and
A23:          s/.k = m1.b1*m2.b2 by A16;
              consider b19,b29 being bag of n such that
A24:          (decomp b)/.k = <*b19,b29*> and
A25:          b = b19+b29 by A17,A21,PRE_POLY:68;
A26:          b2 = <*b19, b29*>.2 by A22,A24,FINSEQ_1:44
                .= b29 by FINSEQ_1:44;
A27:          b1 = <*b19, b29*>.1 by A22,A24,FINSEQ_1:44
                .= b19 by FINSEQ_1:44;
              now
                per cases by A19,A25,A27,A26;
                case
                  b1 <> mb1;
                  then m1.b1 = 0.L by A10;
                  hence m1.b1*m2.b2 = 0.L by BINOM:1;
                end;
                case
                  b2 <> mb2;
                  then m2.b2 = 0.L by A5;
                  hence m1.b1*m2.b2 = 0.L by BINOM:2;
                end;
              end;
              hence s/.k = 0.L by A23;
            end;
            now
              per cases;
              case
                dom s = {};
                then s = <*>(the carrier of L) by RELAT_1:41;
                hence (m1*'m2).b = 0.L by A15;
              end;
              case
A28:            dom s <> {};
                set k = the Element of dom s;
A29:            k in dom s by A28;
                for k9 being Element of NAT st k9 in dom s & k9 <> k
                holds s/.k9 = 0.L by A20;
                then s/.k = (m1*'m2).b by A14,A29,POLYNOM2:3;
                hence (m1*'m2).b = 0.L by A20,A29;
              end;
            end;
            hence contradiction by A13,POLYNOM1:def 3;
          end;
          now
            let b9 be bag of n;
            assume
A30:        b9 <> b;
            consider s being FinSequence of L such that
A31:        (m1*'m2).b9 = Sum s and
A32:        len s = len decomp b9 and
A33:        for k being Element of NAT st k in dom s ex b1, b2 being
bag of n st (decomp b9)/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by POLYNOM1:def 9
            ;
A34:        dom s = Seg(len decomp b9) by A32,FINSEQ_1:def 3
              .= dom(decomp b9) by FINSEQ_1:def 3;
A35:        now
              let k be Element of NAT;
              assume
A36:          k in dom s;
              then consider b1, b2 being bag of n such that
A37:          (decomp b9)/.k = <*b1,b2*> and
A38:          s/.k = m1.b1*m2.b2 by A33;
              consider b19,b29 being bag of n such that
A39:          (decomp b9)/.k = <*b19,b29*> and
A40:          b9 = b19+b29 by A34,A36,PRE_POLY:68;
A41:          b2 = <*b19, b29*>.2 by A37,A39,FINSEQ_1:44
                .= b29 by FINSEQ_1:44;
A42:          b1 = <*b19, b29*>.1 by A37,A39,FINSEQ_1:44
                .= b19 by FINSEQ_1:44;
              now
                per cases by A18,A30,A40,A42,A41;
                case
                  b1 <> mb1;
                  then m1.b1 = 0.L by A10;
                  hence m1.b1*m2.b2 = 0.L by BINOM:1;
                end;
                case
                  b2 <> mb2;
                  then m2.b2 = 0.L by A5;
                  hence m1.b1*m2.b2 = 0.L by BINOM:2;
                end;
              end;
              hence s/.k = 0.L by A38;
            end;
            now
              per cases;
              case
                dom s = {};
                then s = <*>(the carrier of L) by RELAT_1:41;
                hence (m1*'m2).b9 = 0.L by A32;
              end;
              case
A43:            dom s <> {};
                set k = the Element of dom s;
A44:            k in dom s by A43;
                for k9 being Element of NAT st k9 in dom s & k9 <> k
                holds s/.k9 = 0.L by A35;
                then s/.k = (m1*'m2).b9 by A31,A44,POLYNOM2:3;
                hence (m1*'m2).b9 = 0.L by A35,A44;
              end;
            end;
            hence (m1*'m2).b9 = 0.L;
          end;
          hence thesis by POLYNOM7:def 3;
        end;
        case
A45:      Support(m1) = {} or Support(m2) = {};
          now
            per cases by A45;
            case
              Support(m1) = {};
              then m1 = 0_(n,L) by POLYNOM7:1;
              hence thesis by Th2;
            end;
            case
              Support(m2) = {};
              then m2 = 0_(n,L) by POLYNOM7:1;
              hence thesis by POLYNOM1:28;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
  end;
end;

registration
  let n be Ordinal, L be add-associative right_complementable right_zeroed
  distributive non empty doubleLoopStr, c1,c2 be ConstPoly of n,L;
  cluster c1 *' c2 -> Constant;
  coherence
  proof
    set p = c1 *' c2;
    now
      let b be bag of n;
      assume
A1:   b <> EmptyBag n;
      consider s being FinSequence of L such that
A2:   p.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 = c1.b1*c2.b2 by POLYNOM1:def 9;
A5:   dom s = Seg len decomp b by A3,FINSEQ_1:def 3
        .= dom decomp b by FINSEQ_1:def 3;
A6:   now
        let k be Element of NAT;
        assume
A7:     k in dom s;
        then consider b1, b2 being bag of n such that
A8:     (decomp b)/.k = <*b1,b2*> and
A9:     s/.k = c1.b1*c2.b2 by A4;
        consider b19,b29 being bag of n such that
A10:    (decomp b)/.k = <*b19,b29*> and
A11:    b = b19+b29 by A5,A7,PRE_POLY:68;
A12:    b2 = <*b19, b29*>.2 by A8,A10,FINSEQ_1:44
          .= b29 by FINSEQ_1:44;
        b1 = <*b19, b29*>.1 by A8,A10,FINSEQ_1:44
          .= b19 by FINSEQ_1:44;
        then
A13:    b1 <> EmptyBag n or b2 <> EmptyBag n by A1,A11,A12,PRE_POLY:53;
        now
          per cases by A13,POLYNOM7:def 7;
          case
            c1.b1 = 0.L;
            hence s/.k = 0.L by A9,BINOM:1;
          end;
          case
            c2.b2 = 0.L;
            hence s/.k = 0.L by A9,BINOM:2;
          end;
        end;
        hence s/.k = 0.L;
      end;
      now
        per cases;
        case
          dom s = {};
          then s = <*>(the carrier of L) by RELAT_1:41;
          hence p.b = 0.L by A3;
        end;
        case
A14:      dom s <> {};
          set k = the Element of dom s;
A15:      k in dom s by A14;
          for k9 being Element of NAT st k9 in dom s & k9 <> k holds s/.
          k9 = 0.L by A6;
          then Sum s = s/.k by A15,POLYNOM2:3;
          hence p.b = 0.L by A2,A6,A15;
        end;
      end;
      hence p.b = 0.L;
    end;
    hence thesis by POLYNOM7:def 7;
  end;
end;

theorem Th3:
  for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
b,b9 being bag of n, a,a9 being non zero Element of L holds Monom(a * a9,b + b9
  ) = Monom(a,b) *' Monom(a9,b9)
proof
  let n be Ordinal, L be add-associative right_complementable right_zeroed
well-unital distributive domRing-like non trivial doubleLoopStr, b,b9 be bag
  of n, a,a9 be non zero Element of L;
  set m1 = Monom(a,b), m2 = Monom(a9,b9);
  set m = Monom(a * a9,b + b9);
  set m3 = m1 *' m2;
  consider s being FinSequence of L such that
A1: m3.(b+b9) = Sum s and
A2: len s = len decomp(b+b9) and
A3: for k being Element of NAT st k in dom s ex b1, b2 being bag of n
  st (decomp(b+b9))/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by POLYNOM1:def 9;
  set u = b+b9;
  consider k9 being Element of NAT such that
A4: k9 in dom decomp u and
A5: (decomp u)/.k9 = <*b,b9*> by PRE_POLY:69;
A6: dom s = Seg(len decomp(b+b9)) by A2,FINSEQ_1:def 3
    .= dom(decomp(b+b9)) by FINSEQ_1:def 3;
  then consider b1,b2 being bag of n such that
A7: (decomp u)/.k9 = <*b1, b2*> and
A8: s/.k9 = m1.b1*m2.b2 by A3,A4;
A9: b1 = <*b,b9*>.1 by A5,A7,FINSEQ_1:44
    .= b by FINSEQ_1:44;
A10: b2 = <*b,b9*>.2 by A5,A7,FINSEQ_1:44
    .= b9 by FINSEQ_1:44;
A11: m2.b9 = m2.(term(m2)) by POLYNOM7:10
    .= coefficient(m2) by POLYNOM7:def 6
    .= a9 by POLYNOM7:9;
A12: now
A13: m2.b9 <> 0.L by A11;
    let u be bag of n;
    assume
A14: u <> b9;
    consider v being bag of n such that
A15: for b9 being bag of n st b9 <> v holds m2.b9 = 0.L by POLYNOM7:def 3;
    assume m2.u <> 0.L;
    then u = v by A15;
    hence contradiction by A14,A15,A13;
  end;
  a * a9 <> 0.L by VECTSP_2:def 1;
  then
A16: a * a9 is non zero by STRUCT_0:def 12;
A17: m1.b = m1.(term(m1)) by POLYNOM7:10
    .= coefficient(m1) by POLYNOM7:def 6
    .= a by POLYNOM7:9;
A18: now
A19: m1.b <> 0.L by A17;
    let u be bag of n;
    assume
A20: u <> b;
    consider v being bag of n such that
A21: for b9 being bag of n st b9 <> v holds m1.b9 = 0.L by POLYNOM7:def 3;
    assume m1.u <> 0.L;
    then u = v by A21;
    hence contradiction by A20,A21,A19;
  end;
A22: now
    let k be Element of NAT;
    assume that
A23: k in dom s and
A24: k <> k9;
    consider b1,b2 being bag of n such that
A25: (decomp u)/.k = <*b1, b2*> and
A26: s/.k = m1.b1*m2.b2 by A3,A23;
A27: now
      assume
A28:  b1 = b & b2 = b9;
      (decomp u).k = (decomp u)/.k by A6,A23,PARTFUN1:def 6
        .= (decomp u).k9 by A4,A5,A25,A28,PARTFUN1:def 6;
      hence contradiction by A6,A4,A23,A24,FUNCT_1:def 4;
    end;
    now
      per cases by A27;
      case
        b1 <> b;
        then m1.b1 = 0.L by A18;
        hence m1.b1 * m2.b2 = 0.L by BINOM:1;
      end;
      case
        b2 <> b9;
        then m2.b2 = 0.L by A12;
        hence m1.b1*m2.b2 = 0.L by BINOM:2;
      end;
    end;
    hence s/.k = 0.L by A26;
  end;
  then Sum s = s/.k9 by A6,A4,POLYNOM2:3;
  then
A29: m3.(b+b9) <> 0.L by A17,A11,A1,A8,A9,A10,VECTSP_2:def 1;
  then
A30: term(m3) = b + b9 by POLYNOM7:def 5
    .= term(m) by A16,POLYNOM7:10;
A31: coefficient(m3) = m3.(term m3) by POLYNOM7:def 6
    .= m3.(b+b9) by A29,POLYNOM7:def 5
    .= a * a9 by A17,A11,A1,A6,A4,A8,A9,A10,A22,POLYNOM2:3
    .= coefficient(m) by POLYNOM7:9;
  thus m = Monom(coefficient(m),term(m)) by POLYNOM7:11
    .= m3 by A30,A31,POLYNOM7:11;
end;

theorem
  for n being Ordinal, L being add-associative right_complementable
right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr,
  a,a9 being Element of L holds (a * a9) |(n,L) = (a |(n,L)) *' (a9 |(n,L))
proof
  let n be Ordinal, L be add-associative right_complementable right_zeroed
  well-unital distributive domRing-like non trivial doubleLoopStr, a,a9 be
  Element of L;
  per cases;
  suppose
A1: a is non zero & a9 is non zero;
    term((a*a9) |(n,L)) = EmptyBag n & coefficient((a*a9) |(n,L)) = a*a9
    by POLYNOM7:23;
    then
A2: (a * a9) |(n,L) = Monom(a*a9,EmptyBag n) by POLYNOM7:11;
    term(a9 |(n,L)) = EmptyBag n & coefficient(a9 |(n,L)) = a9 by POLYNOM7:23;
    then
A3: a9 |(n,L) = Monom(a9,EmptyBag n) by POLYNOM7:11;
    term(a |(n,L)) = EmptyBag n & coefficient(a |(n,L)) = a by POLYNOM7:23;
    then
A4: a |(n,L) = Monom(a,EmptyBag n) by POLYNOM7:11;
    EmptyBag n + EmptyBag n = EmptyBag n by PRE_POLY:53;
    hence thesis by A1,A2,A4,A3,Th3;
  end;
  suppose
A5: not(a is non zero & a9 is non zero);
    now
      per cases by A5,STRUCT_0:def 12;
      case
A6:     a = 0.L;
        then a * a9 = 0.L by BINOM:1;
        then
A7:     (a * a9) |(n,L) = 0_(n,L) by POLYNOM7:19;
        a |(n,L) = 0_(n,L) by A6,POLYNOM7:19;
        hence thesis by A7,Th2;
      end;
      case
A8:     a9 = 0.L;
        then a * a9 = 0.L by BINOM:2;
        then
A9:     (a * a9) |(n,L) = 0_(n,L) by POLYNOM7:19;
        a9 |(n,L) = 0_(n,L) by A8,POLYNOM7:19;
        hence thesis by A9,POLYNOM1:28;
      end;
    end;
    hence thesis;
  end;
end;

begin :: Term Orders

Lm1: for n being Ordinal, T being TermOrder of n, b being set st b in field T
holds b is bag of n
proof
  let n be Ordinal, T be TermOrder of n, b be set;
  assume b in field T;
  then
A1: b in dom T \/ rng T by RELAT_1:def 6;
  per cases by A1,XBOOLE_0:def 3;
  suppose
    b in dom T;
    then b is Element of Bags n;
    hence thesis;
  end;
  suppose
    b in rng T;
    then b is Element of Bags n;
    hence thesis;
  end;
end;

registration
  let n be Ordinal;
  cluster admissible connected for TermOrder of n;
  existence
  proof
    set T = LexOrder n;
    take T;
    now
      let x,y be set;
      assume that
A1:   x in field T & y in field T and
      x <> y;
      reconsider b1 = x, b2 = y as bag of n by A1,Lm1;
      b1 <=' b2 or b2 <=' b1 by PRE_POLY:45;
      hence [x,y] in T or [y,x] in T by PRE_POLY:def 14;
    end;
    then T is_connected_in field T by RELAT_2:def 6;
    hence thesis by RELAT_2:def 14;
  end;
end;

:: theorem 5.5 (ii), p. 190

registration
  let n be Nat;
  cluster -> well_founded for admissible TermOrder of n;
  coherence
  proof
    let T be admissible TermOrder of n;
    T is well-ordering by BAGORDER:34;
    hence thesis by WELLORD1:def 4;
  end;
end;

definition
  let n be Ordinal, T be TermOrder of n, b,b9 be bag of n;
  pred b <= b9,T means
  :Def2:
  [b,b9] in T;
end;

definition
  let n be Ordinal, T be TermOrder of n, b,b9 be bag of n;
  pred b < b9,T means
  :Def3:
  b <= b9,T & b <> b9;
end;

definition
  let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n;
  func min(b1,b2,T) -> bag of n equals
  :Def4:
  b1 if b1 <= b2,T otherwise b2;
  correctness;
  func max(b1,b2,T) -> bag of n equals
  :Def5:
  b1 if b2 <= b1,T otherwise b2;
  correctness;
end;

Lm2: for n being Ordinal, T being TermOrder of n, b being bag of n holds b <=
b,T
proof
  let n be Ordinal, T be TermOrder of n, b be bag of n;
  field T = Bags n by ORDERS_1:12;
  then
A1: T is_reflexive_in Bags n by RELAT_2:def 9;
  b is Element of Bags n by PRE_POLY:def 12;
  then [b,b] in T by A1,RELAT_2:def 1;
  hence thesis by Def2;
end;

Lm3: for n being Ordinal, T being TermOrder of n, b1,b2 being bag of n st b1
<= b2,T & b2 <= b1,T holds b1 = b2
proof
  let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n;
  field T = Bags n by ORDERS_1:12;
  then
A1: T is_antisymmetric_in Bags n by RELAT_2:def 12;
  assume b1 <= b2,T & b2 <= b1,T;
  then
A2: [b1,b2] in T & [b2,b1] in T by Def2;
  b1 is Element of Bags n & b2 is Element of Bags n by PRE_POLY:def 12;
  hence thesis by A2,A1,RELAT_2:def 4;
end;

Lm4: for n being Ordinal, T being TermOrder of n, b being bag of n holds b in
field T
proof
  let n be Ordinal, T be TermOrder of n, b be bag of n;
  field T = Bags n by ORDERS_1:12;
  then
A1: T is_reflexive_in Bags n by RELAT_2:def 9;
  b is Element of Bags n by PRE_POLY:def 12;
  then [b,b] in T by A1,RELAT_2:def 1;
  hence thesis by RELAT_1:15;
end;

theorem Th5:
  for n being Ordinal, T being connected TermOrder of n, b1,b2
  being bag of n holds b1 <= b2,T iff not b2 < b1,T
proof
  let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n;
A1: T is_connected_in field T by RELAT_2:def 14;
  per cases;
  suppose
    b1 = b2;
    hence thesis by Def3,Lm2;
  end;
  suppose
A2: b1 <> b2;
A3: not b2 < b1,T implies b1 <= b2,T
    proof
      assume
A4:   not b2 < b1,T;
      now
        per cases by A4,Def3;
        case
A5:       not b2 <= b1,T;
A6:       b1 in field T & b2 in field T by Lm4;
          not [b2,b1] in T by A5,Def2;
          then [b1,b2] in T by A1,A2,A6,RELAT_2:def 6;
          hence thesis by Def2;
        end;
        case
          b1 = b2;
          hence thesis by A2;
        end;
      end;
      hence thesis;
    end;
    b1 <= b2,T implies not b2 < b1,T
    proof
      assume
A7:   b1 <= b2,T;
      assume b2 < b1,T;
      then b2 <= b1,T & b1 <> b2 by Def3;
      hence thesis by A7,Lm3;
    end;
    hence thesis by A3;
  end;
end;

Lm5: for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of
n holds b1 <= b2,T or b2 <= b1,T
proof
  let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n;
A1: T is_connected_in field T by RELAT_2:def 14;
  per cases;
  suppose
A2: b1 = b2;
    field T = Bags n by ORDERS_1:12;
    then
A3: T is_reflexive_in Bags n by RELAT_2:def 9;
    b1 is Element of Bags n by PRE_POLY:def 12;
    then [b1,b2] in T by A2,A3,RELAT_2:def 1;
    hence thesis by Def2;
  end;
  suppose
A4: b1 <> b2;
    assume not b1 <= b2,T;
    then
A5: not [b1,b2] in T by Def2;
    b1 in field T & b2 in field T by Lm4;
    then [b2,b1] in T by A1,A4,A5,RELAT_2:def 6;
    hence thesis by Def2;
  end;
end;

theorem
  for n being Ordinal, T being TermOrder of n, b being bag of n holds b
  <= b,T by Lm2;

theorem
  for n being Ordinal, T being TermOrder of n, b1,b2 being bag of n st
  b1 <= b2,T & b2 <= b1,T holds b1 = b2 by Lm3;

theorem Th8:
  for n being Ordinal, T being TermOrder of n, b1,b2,b3 being bag
  of n st b1 <= b2,T & b2 <= b3,T holds b1 <= b3,T
proof
  let n be Ordinal, T be TermOrder of n, b1,b2,b3 be bag of n;
A1: b3 is Element of Bags n by PRE_POLY:def 12;
  field T = Bags n by ORDERS_1:12;
  then
A2: T is_transitive_in Bags n by RELAT_2:def 16;
  assume b1 <= b2,T & b2 <= b3,T;
  then
A3: [b1,b2] in T & [b2,b3] in T by Def2;
  b1 is Element of Bags n & b2 is Element of Bags n by PRE_POLY:def 12;
  then [b1,b3] in T by A3,A2,A1,RELAT_2:def 8;
  hence thesis by Def2;
end;

theorem Th9:
  for n being Ordinal, T being admissible TermOrder of n, b being
  bag of n holds EmptyBag n <= b,T
proof
  let n be Ordinal, T be admissible TermOrder of n, b be bag of n;
  [EmptyBag n,b] in T by BAGORDER:def 5;
  hence thesis by Def2;
end;

theorem
  for n being Ordinal, T being admissible TermOrder of n, b1,b2 being
  bag of n holds b1 divides b2 implies b1 <= b2,T
proof
  let n be Ordinal, T be admissible TermOrder of n, b1,b2 be bag of n;
  assume b1 divides b2;
  then consider b3 being bag of n such that
A1: b2 = b1 + b3 by Th1;
  EmptyBag n <= b3,T by Th9;
  then [EmptyBag n,b3] in T by Def2;
  then [EmptyBag n + b1,b2] in T by A1,BAGORDER:def 5;
  then [b1,b2] in T by PRE_POLY:53;
  hence thesis by Def2;
end;

theorem Th11:
  for n being Ordinal, T being TermOrder of n, b1,b2 being bag of
  n holds min(b1,b2,T) = b1 or min(b1,b2,T) = b2
proof
  let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n;
  assume
A1: min(b1,b2,T) <> b1;
  now
    per cases by A1,Def4;
    case
      not b1 <= b2,T;
      hence thesis by Def4;
    end;
    case
      b1 = b2;
      then b1 <= b2,T by Lm2;
      hence contradiction by A1,Def4;
    end;
  end;
  hence thesis;
end;

theorem Th12:
  for n being Ordinal, T being TermOrder of n, b1,b2 being bag of
  n holds max(b1,b2,T) = b1 or max(b1,b2,T) = b2
proof
  let n be Ordinal, T be TermOrder of n, b1,b2 be bag of n;
  assume
A1: max(b1,b2,T) <> b1;
  now
    per cases by A1,Def5;
    case
      not b2 <= b1,T;
      hence thesis by Def5;
    end;
    case
      b1 = b2;
      then b2 <= b1,T by Lm2;
      hence contradiction by A1,Def5;
    end;
  end;
  hence thesis;
end;

Lm6: for n being Ordinal, T being TermOrder of n, b being bag of n holds min(b
,b,T) = b & max(b,b,T) = b
proof
  let n being Ordinal, T being TermOrder of n, b being bag of n;
  thus min(b,b,T) = b by Def4;
  thus thesis by Def5;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag
  of n holds min(b1,b2,T) <= b1,T & min(b1,b2,T) <= b2,T
proof
  let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n;
  per cases by Lm5;
  suppose
A1: b1 <= b2,T;
    then min(b1,b2,T) = b1 by Def4;
    hence thesis by A1,Lm2;
  end;
  suppose
A2: b2 <= b1,T;
    now
      per cases;
      case
A3:     b1 = b2;
        then min(b1,b2,T) = b1 by Lm6;
        hence thesis by A3,Lm2;
      end;
      case
        b1 <> b2;
        then b2 < b1,T by A2,Def3;
        then not b1 <= b2,T by Th5;
        then min(b1,b2,T) = b2 by Def4;
        hence thesis by A2,Lm2;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th14:
  for n being Ordinal, T being connected TermOrder of n, b1,b2
  being bag of n holds b1 <= max(b1,b2,T),T & b2 <= max(b1,b2,T),T
proof
  let n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n;
  per cases by Lm5;
  suppose
A1: b2 <= b1,T;
    then max(b1,b2,T) = b1 by Def5;
    hence thesis by A1,Lm2;
  end;
  suppose
A2: b1 <= b2,T;
    now
      per cases;
      case
A3:     b1 = b2;
        then max(b1,b2,T) = b1 by Lm6;
        hence thesis by A3,Lm2;
      end;
      case
        b1 <> b2;
        then b1 < b2,T by A2,Def3;
        then not b2 <= b1,T by Th5;
        then max(b1,b2,T) = b2 by Def5;
        hence thesis by A2,Lm2;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th15:
  for n being Ordinal, T being connected TermOrder of n, b1,b2
being bag of n holds min(b1,b2,T) = min(b2,b1,T) & max(b1,b2,T) = max(b2,b1,T)
proof
  let n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n;
  now
    per cases;
    case
A1:   min(b1,b2,T) = b1;
      now
        per cases by A1,Def4;
        case
A2:       b1 <= b2,T;
          now
            per cases;
            case
              b1 = b2;
              hence min(b2,b1,T) = min(b1,b2,T);
            end;
            case
              b1 <> b2;
              then not b2 <= b1,T by A2,Lm3;
              hence min(b2,b1,T) = min(b1,b2,T) by A1,Def4;
            end;
          end;
          hence min(b1,b2,T) = min(b2,b1,T);
        end;
        case
          b1 = b2;
          hence min(b2,b1,T) = min(b1,b2,T);
        end;
      end;
      hence min(b1,b2,T) = min(b2,b1,T);
    end;
    case
A3:   min(b1,b2,T) <> b1;
A4:   now
        assume not b2 <= b1,T;
        then b1 <= b2,T by Lm5;
        hence contradiction by A3,Def4;
      end;
      thus min(b1,b2,T) = b2 by A3,Th11
        .= min(b2,b1,T) by A4,Def4;
    end;
  end;
  hence min(b1,b2,T) = min(b2,b1,T);
  now
    per cases;
    case
A5:   max(b1,b2,T) = b1;
      now
        per cases by A5,Def5;
        case
A6:       b2 <= b1,T;
          now
            per cases;
            case
              b1 = b2;
              hence max(b2,b1,T) = max(b1,b2,T);
            end;
            case
              b1 <> b2;
              then not b1 <= b2,T by A6,Lm3;
              hence max(b2,b1,T) = max(b1,b2,T) by A5,Def5;
            end;
          end;
          hence thesis;
        end;
        case
          b1 = b2;
          hence max(b2,b1,T) = max(b1,b2,T);
        end;
      end;
      hence thesis;
    end;
    case
A7:   max(b1,b2,T) <> b1;
      now
        per cases by Lm5;
        case
          b1 <= b2,T;
          hence max(b2,b1,T) = b2 by Def5
            .= max(b1,b2,T) by A7,Th12;
        end;
        case
          b2 <= b1,T;
          hence max(b2,b1,T) = max(b1,b2,T) by A7,Def5;
        end;
      end;
      hence max(b2,b1,T) = max(b1,b2,T);
    end;
  end;
  hence thesis;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, b1,b2 being bag
  of n holds min(b1,b2,T) = b1 iff max(b1,b2,T) = b2
proof
  let n being Ordinal, T being connected TermOrder of n, b1,b2 being bag of n;
A1: now
    assume
A2: max(b1,b2,T) = b2;
    now
      per cases by A2,Def5;
      case
        not b2 <= b1,T;
        then b1 <= b2,T by Lm5;
        hence min(b1,b2,T) = b1 by Def4;
      end;
      case
        b1 = b2;
        hence min(b1,b2,T) = b1 by Th11;
      end;
    end;
    hence min(b1,b2,T) = b1;
  end;
  now
    assume
A3: min(b1,b2,T) = b1;
    now
      per cases by A3,Def4;
      case
        b1 <= b2,T;
        then max(b2,b1,T) = b2 by Def5;
        hence max(b1,b2,T) = b2 by Th15;
      end;
      case
        b1 = b2;
        hence max(b1,b2,T) = b2 by Th12;
      end;
    end;
    hence max(b1,b2,T) = b2;
  end;
  hence thesis by A1;
end;

begin :: Headterms, Headmonomials and Headcoefficients

definition
  let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p
  be Polynomial of n,L;
  func HT(p,T) -> Element of Bags n means
  :Def6:
  Support p = {} & it =
EmptyBag n or (it in Support p & for b being bag of n st b in Support p holds b
  <= it,T);
  existence
  proof
    set O = T;
    per cases;
    suppose
      Support p = {};
      hence thesis;
    end;
    suppose
A1:   Support p <> {};
      reconsider sp = Support p as finite set by POLYNOM1:def 4;
      card sp is finite;
      then consider m being Nat such that
A2:   card(Support p) = card m by CARD_1:48;
      reconsider sp = Support p as finite Subset of Bags n by POLYNOM1:def 4;
      defpred P[Nat] means for B being finite Subset of Bags n st card B = $1
holds ex b9 being bag of n st b9 in B & for b being bag of n st b in B holds [b
      ,b9] in O;
A3:   for k being Nat st 1 <= k holds P[k] implies P[k+1]
      proof
        let k be Nat;
        assume
A4:     1 <= k;
        thus P[k] implies P[k+1]
        proof
          assume
A5:       P[k];
          thus P[k+1]
          proof
            let B be finite Subset of Bags n;
            assume
A6:         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 set;
              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
A7:         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
A8:         card(X) + 1 = k + 1 by A6,A7,CARD_2:41,TARSKI:def 1;
            then reconsider X as non empty set by A4;
            consider b9 being bag of n such that
A9:         b9 in X and
A10:        for b being bag of n st b in X holds [b,b9] in O by A5,A8;
A11:        O is_connected_in field O by RELAT_2:def 14;
            now
              per cases;
              case
A12:            x = b9;
A13:            now
                  let b be bag of n;
                  assume
A14:              b in B;
                  now
                    per cases;
                    case
                      b in X;
                      hence [b,b9] in O by A10;
                    end;
                    case
                      not b in X;
                      then b in {x} by A7,A14,XBOOLE_0:def 3;
                      then b = x by TARSKI:def 1;
                      hence [b,b9] in O by A12,ORDERS_1:3;
                    end;
                  end;
                  hence [b,b9] in O;
                end;
                take b9;
                X c= B by XBOOLE_1:36;
                hence thesis by A9,A13;
              end;
              case
A15:            x <> b9;
                b9 is Element of Bags n by PRE_POLY:def 12;
                then [b9,b9] in O by ORDERS_1:3;
                then
A16:            b9 in field O by RELAT_1:15;
                [x,x] in O by ORDERS_1:3;
                then
A17:            x in field O by RELAT_1:15;
                now
                  per cases by A11,A15,A17,A16,RELAT_2:def 6;
                  case
A18:                [x,b9] in O;
                    thus ex b9 being bag of n st b9 in B & for b being bag of
                    n st b in B holds [b,b9] in O
                    proof
                      take b9;
                      for b being bag of n st b in B holds [b,b9] in O
                      proof
                        let b be bag of n;
                        assume
A19:                    b in B;
                        now
                          per cases;
                          case
                            b <> x;
                            then not b in {x} by TARSKI:def 1;
                            then b in X by A19,XBOOLE_0:def 5;
                            hence thesis by A10;
                          end;
                          case
                            b = x;
                            hence thesis by A18;
                          end;
                        end;
                        hence thesis;
                      end;
                      hence thesis by A9,XBOOLE_0:def 5;
                    end;
                  end;
                  case
A20:                [b9,x] in O;
                    thus ex b9 being bag of n st b9 in B & for b being bag of
                    n st b in B holds [b,b9] in O
                    proof
                      take x;
                      for b being bag of n st b in B holds [b,x] in O
                      proof
                        let b be bag of n;
                        assume
A21:                    b in B;
                        now
                          per cases;
                          case
                            b <> x;
                            then not b in {x} by TARSKI:def 1;
                            then b in X by A21,XBOOLE_0:def 5;
                            then
A22:                        [b,b9] in O by A10;
                            b is Element of Bags n & b9 is Element of
                            Bags n by PRE_POLY:def 12;
                            hence thesis by A20,A22,ORDERS_1:5;
                          end;
                          case
                            b = x;
                            hence thesis by ORDERS_1:3;
                          end;
                        end;
                        hence thesis;
                      end;
                      hence thesis;
                    end;
                  end;
                end;
                hence thesis;
              end;
            end;
            hence thesis;
          end;
        end;
      end;
      m <> 0 by A1,A2;
      then
A23:  1 <= m by NAT_1:14;
A24:  card(Support p) = m by A2,CARD_1:def 2;
A25:  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 set such that
A26:    B = {b} by CARD_1:29;
A27:    b in B by A26,TARSKI:def 1;
        then reconsider b as Element of Bags n;
        reconsider b as bag of n;
        now
          let b9 be bag of n;
          assume b9 in B;
          then b9 = b by A26,TARSKI:def 1;
          hence [b9,b] in O by ORDERS_1:3;
        end;
        hence thesis by A27;
      end;
      for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(A25,A3);
      then consider b9 being bag of n such that
A28:  b9 in sp and
A29:  for b being bag of n st b in sp holds [b,b9] in O by A24,A23;
      take b9;
      now
        let b be bag of n;
        assume b in sp;
        then [b,b9] in O by A29;
        hence b <= b9,O by Def2;
      end;
      hence thesis by A28;
    end;
  end;
  uniqueness
  proof
    let b1,b2 be Element of Bags n;
    set O = T;
    assume
A30: Support p = {} & b1 = EmptyBag n or (b1 in Support p & for b
    being bag of n st b in Support p holds b <= b1,O);
    assume
A31: Support p = {} & b2 = EmptyBag n or (b2 in Support p & for b
    being bag of n st b in Support p holds b <= b2,O);
    per cases;
    suppose
      Support p = {};
      hence b1 = b2 by A30,A31;
    end;
    suppose
A32:  Support p <> {};
      then b1 <= b2,O by A30,A31;
      then
A33:  [b1,b2] in O by Def2;
      b2 <= b1,O by A30,A31,A32;
      then [b2,b1] in O by Def2;
      hence b1 = b2 by A33,ORDERS_1:4;
    end;
  end;
end;

definition :: definition 5.15, p. 194
  let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p
  be Polynomial of n,L;
  func HC(p,T) -> Element of L equals
  p.(HT(p,T));
  correctness;
end;

definition :: definition 5.15, p. 194
  let n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, p
  be Polynomial of n,L;
  func HM(p,T) -> Monomial of n,L equals
  Monom(HC(p,T),HT(p,T));
  correctness;
end;

Lm7: for n being Ordinal, O be connected TermOrder of n, L be non empty
ZeroStr, p be Polynomial of n,L holds HC(p,O) = 0.L iff p = 0_(n,L)
proof
  let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, p
  be Polynomial of n,L;
  now
    assume HC(p,O) = 0.L;
    then not HT(p,O) in Support p by POLYNOM1:def 3;
    then Support p = {} by Def6;
    hence p = 0_(n,L) by POLYNOM7:1;
  end;
  hence thesis by POLYNOM1:22;
end;

Lm8: for n being Ordinal, O be connected TermOrder of n, L be non trivial
ZeroStr, p be Polynomial of n,L holds (HM(p,O)).(HT(p,O)) = p.(HT(p,O))
proof
  let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr
  , p be Polynomial of n,L;
A1: now
    per cases;
    case
      HC(p,O) <> 0.L;
      then HC(p,O) is non zero by STRUCT_0:def 12;
      hence term(HM(p,O)) = HT(p,O) by POLYNOM7:10;
    end;
    case
A2:   HC(p,O) = 0.L;
      then p = 0_(n,L) by Lm7;
      then Support p = {} by POLYNOM7:1;
      then HT(p,O) = EmptyBag n by Def6;
      hence term(HM(p,O)) = HT(p,O) by A2,POLYNOM7:8;
    end;
  end;
  p.(HT(p,O)) = coefficient(HM(p,O)) by POLYNOM7:9
    .= (HM(p,O)).term(HM(p,O)) by POLYNOM7:def 6;
  hence thesis by A1;
end;

Lm9: for n being Ordinal, O be connected TermOrder of n, L be non trivial
ZeroStr, p be Polynomial of n,L st HC(p,O) <> 0.L holds HT(p,O) in Support(HM(p
,O))
proof
  let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr
  , p be Polynomial of n,L;
  assume HC(p,O) <> 0.L;
  then (HM(p,O)).(HT(p,O)) <> 0.L by Lm8;
  hence thesis by POLYNOM1:def 3;
end;

Lm10: for n being Ordinal, O be connected TermOrder of n, L be non trivial
ZeroStr, p be Polynomial of n,L st HC(p,O) = 0.L holds Support(HM(p,O)) = {}
proof
  let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr
  , p be Polynomial of n,L;
  assume
A1: HC(p,O) = 0.L;
  then p = 0_(n,L) by Lm7;
  then Support p = {} by POLYNOM7:1;
  then
A2: HT(p,O) = EmptyBag n by Def6;
A3: term(HM(p,O)) = EmptyBag n by A1,POLYNOM7:8;
  now
    assume Support(HM(p,O)) <> {};
    then Support(HM(p,O)) = {term(HM(p,O))} by POLYNOM7:7;
    then term(HM(p,O)) in Support(HM(p,O)) by TARSKI:def 1;
    then (HM(p,O)).EmptyBag n <> 0.L by A3,POLYNOM1:def 3;
    hence contradiction by A1,A2,Lm8;
  end;
  hence thesis;
end;

registration
  let n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p
  be non-zero Polynomial of n,L;
  cluster HM(p,T) -> non-zero;
  coherence
  proof
    set O = T;
    now
      per cases;
      case
        HC(p,O) <> 0.L;
        then HT(p,O) in Support(HM(p,O)) by Lm9;
        then HM(p,O) <> 0_(n,L) by POLYNOM7:1;
        hence thesis by POLYNOM7:def 1;
      end;
      case
        HC(p,O) = 0.L;
        then p = 0_(n,L) by Lm7;
        hence thesis by POLYNOM7:def 1;
      end;
    end;
    hence thesis;
  end;
  cluster HC(p,T) -> non zero;
  coherence
  proof
    set O = T, a = HC(p,O);
    now
      assume a = 0.L;
      then not(HT(p,O)) in Support p by POLYNOM1:def 3;
      then Support p = {} by Def6;
      then p = 0_(n,L) by POLYNOM7:1;
      hence contradiction by POLYNOM7:def 1;
    end;
    hence thesis by STRUCT_0:def 12;
  end;
end;

Lm11: for n being Ordinal, O be connected TermOrder of n, L be non empty
ZeroStr, m being Monomial of n,L holds HT(m,O) = term(m) & HC(m,O) =
coefficient(m) & HM(m,O) = m
proof
  let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, m
  be Monomial of n,L;
  per cases by POLYNOM7:6;
  suppose
A1: Support m = {};
    hence
A2: term(m) = EmptyBag n by POLYNOM7:def 5
      .= HT(m,O) by A1,Def6;
    hence HC(m,O) = coefficient(m) by POLYNOM7:def 6;
    hence thesis by A2,POLYNOM7:11;
  end;
  suppose
A3: ex b being bag of n st Support m = {b};
    then consider b being bag of n such that
A4: Support m = {b};
    b in Support m by A4,TARSKI:def 1;
    then
A5: m.b <> 0.L by POLYNOM1:def 3;
    HT(m,O) in Support m by A3,Def6;
    hence
A6: HT(m,O) = b by A4,TARSKI:def 1
      .= term(m) by A5,POLYNOM7:def 5;
    hence HC(m,O) = coefficient(m) by POLYNOM7:def 6;
    hence thesis by A6,POLYNOM7:11;
  end;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
empty ZeroStr, p being Polynomial of n,L holds HC(p,T) = 0.L iff p = 0_(n,L)
by Lm7;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
trivial ZeroStr, p being Polynomial of n,L holds (HM(p,T)).(HT(p,T)) = p.(HT(p,
  T)) by Lm8;

theorem Th19:
  for n being Ordinal, T being connected TermOrder of n, L being
non trivial ZeroStr, p being Polynomial of n,L, b being bag of n st b <> HT(p,T
  ) holds HM(p,T).b = 0.L
proof
  let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr
  , p be Polynomial of n,L, b being bag of n;
  assume
A1: b <> HT(p,O);
  per cases by POLYNOM7:6;
  suppose
    Support HM(p,O) = {};
    then HM(p,O) = 0_(n,L) by POLYNOM7:1;
    hence thesis by POLYNOM1:22;
  end;
  suppose
    ex b being bag of n st Support HM(p,O) = {b};
    then consider b1 being bag of n such that
A2: Support HM(p,O) = {b1};
A3: b is Element of Bags n by PRE_POLY:def 12;
    now
      per cases;
      case
        HC(p,O) <> 0.L;
        then HT(p,O) in {b1} by A2,Lm9;
        then b1 <> b by A1,TARSKI:def 1;
        then not b in {b1} by TARSKI:def 1;
        hence thesis by A2,A3,POLYNOM1:def 3;
      end;
      case
        HC(p,O) = 0.L;
        then Support(HM(p,O)) = {} by Lm10;
        then HM(p,O) = 0_(n,L) by POLYNOM7:1;
        hence thesis by POLYNOM1:22;
      end;
    end;
    hence thesis;
  end;
end;

Lm12: for n being Ordinal, O be connected TermOrder of n, L be non trivial
ZeroStr, p be Polynomial of n,L holds Support(HM(p,O)) = {} or Support(HM(p,O))
= {HT(p,O)}
proof
  let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p
  be Polynomial of n,L;
  assume
A1: not Support(HM(p,O)) = {};
  then
A2: ex b being bag of n st Support(HM(p,O)) = {b} by POLYNOM7:6;
  now
    per cases;
    case
      HC(p,O) = 0.L;
      hence thesis by A1,Lm10;
    end;
    case
      HC(p,O) <> 0.L;
      then HT(p,O) in Support HM(p,O) by Lm9;
      hence thesis by A2,TARSKI:def 1;
    end;
  end;
  hence thesis;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
trivial ZeroStr, p being Polynomial of n,L holds Support(HM(p,T)) c= Support(p)
proof
  let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p
  be Polynomial of n,L;
  now
    let u be set;
    assume
A1: u in Support(HM(p,O));
    now
      per cases by A1,Lm12;
      case
        u in {};
        hence u in Support p;
      end;
      case
        u in {HT(p,O)};
        then
A2:     u = HT(p,O) by TARSKI:def 1;
        now
          per cases;
          case
            HC(p,O) = 0.L;
            then (HM(p,O)).(HT(p,O)) = 0.L by Lm8;
            hence contradiction by A1,A2,POLYNOM1:def 3;
          end;
          case
            HC(p,O) <> 0.L;
            hence u in Support p by A2,POLYNOM1:def 3;
          end;
        end;
        hence u in Support p;
      end;
    end;
    hence u in Support p;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
  trivial ZeroStr, p being Polynomial of n,L holds Support(HM(p,T)) = {} or
  Support(HM(p,T)) = {HT(p,T)} by Lm12;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
  trivial ZeroStr, p being Polynomial of n,L holds term(HM(p,T)) = HT(p,T) &
  coefficient(HM(p,T)) = HC(p,T)
proof
  let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p
  be Polynomial of n,L;
  per cases;
  suppose
    HC(p,O) is non zero;
    then reconsider a = HC(p,O) as non zero Element of L;
    term(Monom(a,HT(p,O))) = HT(p,O) by POLYNOM7:10;
    hence thesis by POLYNOM7:9;
  end;
  suppose
A1: not HC(p,O) is non zero;
    now
      per cases;
      case
        not p is non-zero;
        then p = 0_(n,L) by POLYNOM7:def 1;
        then Support p = {} by POLYNOM7:1;
        then HT(p,O) = EmptyBag n by Def6
          .= term(Monom(0.L,HT(p,O))) by POLYNOM7:8
          .= term(HM(p,O)) by A1,STRUCT_0:def 12;
        hence thesis by POLYNOM7:9;
      end;
      case
        p is non-zero;
        then reconsider p as non-zero Polynomial of n,L;
        HC(p,O) is non zero;
        hence thesis by A1;
      end;
    end;
    hence thesis;
  end;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
  empty ZeroStr, m being Monomial of n,L holds HT(m,T) = term(m) & HC(m,T) =
  coefficient(m) & HM(m,T) = m by Lm11;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
empty ZeroStr, c being ConstPoly of n,L holds HT(c,T) = EmptyBag n & HC(c,T) =
  c.(EmptyBag n)
proof
  let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, c
  be ConstPoly of n,L;
  thus HT(c,O) = term(c) by Lm11
    .= EmptyBag n by POLYNOM7:16;
  thus HC(c,O) = coefficient(c) by Lm11
    .= c.(EmptyBag n) by POLYNOM7:16;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
empty ZeroStr, a being Element of L holds HT(a |(n,L),T) = EmptyBag n & HC(a |(
  n,L),T) = a
proof
  let n be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, a
  be Element of L;
  set p = a |(n,L);
  thus HT(p,O) = term(p) by Lm11
    .= EmptyBag n by POLYNOM7:23;
  thus HC(p,O) = coefficient(p) by Lm11
    .= a by POLYNOM7:23;
end;

theorem Th26:
  for n being Ordinal, T being connected TermOrder of n, L being
  non trivial ZeroStr, p being Polynomial of n,L holds HT(HM(p,T),T) = HT(p,T)
proof
  let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p
  be Polynomial of n,L;
  per cases;
  suppose
    HC(p,O) is non zero;
    then reconsider a = HC(p,O) as non zero Element of L;
    thus HT(HM(p,O),O) = term(Monom(a,HT(p,O))) by Lm11
      .= HT(p,O) by POLYNOM7:10;
  end;
  suppose
A1: not HC(p,O) is non zero;
    now
      per cases;
      case
        not p is non-zero;
        then p = 0_(n,L) by POLYNOM7:def 1;
        then Support p = {} by POLYNOM7:1;
        then HT(p,O) = EmptyBag n by Def6
          .= term(Monom(0.L,HT(p,O))) by POLYNOM7:8
          .= term(HM(p,O)) by A1,STRUCT_0:def 12;
        hence thesis by Lm11;
      end;
      case
        p is non-zero;
        then reconsider p as non-zero Polynomial of n,L;
        HC(p,O) is non zero;
        hence thesis by A1;
      end;
    end;
    hence thesis;
  end;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
  trivial ZeroStr, p being Polynomial of n,L holds HC(HM(p,T),T) = HC(p,T)
proof
  let n being Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr
  , p being Polynomial of n,L;
  thus HC(HM(p,O),O) = (HM(p,O)).(HT(p,O)) by Th26
    .= HC(p,O) by Lm8;
end;

theorem
  for n being Ordinal, T being connected TermOrder of n, L being non
empty ZeroStr, p being Polynomial of n,L holds HM(HM(p,T),T) = HM(p,T) by Lm11;

Lm13: 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;

Lm14: for n being Ordinal, O be admissible connected TermOrder of n, L being
add-associative right_complementable left_zeroed right_zeroed well-unital
distributive non trivial doubleLoopStr, p,q being non-zero Polynomial of n,L
holds (p*'q).(HT(p,O) + HT(q,O)) = p.(HT(p,O)) * q.(HT(q,O))
proof
  let n be Ordinal, O be admissible connected TermOrder of n, L be
  add-associative right_complementable right_zeroed left_zeroed well-unital
  distributive non trivial doubleLoopStr, p,q be non-zero Polynomial of n,L;
  set b = HT(p,O) + HT(q,O);
  consider s being FinSequence of L such that
A1: (p*'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 = p.b1*q.b2 by POLYNOM1:def 9;
  consider S being non empty finite Subset of Bags n such that
A4: divisors b = SgmX(BagOrder n, S) and
A5: 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);
A6: BagOrder n linearly_orders S by Lm13;
  HT(p,O) divides b by PRE_POLY:50;
  then HT(p,O) in S by A5;
  then HT(p,O) in rng(sgm) by A6,PRE_POLY:def 2;
  then consider i being set such that
A7: i in dom sgm and
A8: sgm.i = HT(p,O) by FUNCT_1:def 3;
A9: i in dom decomp b by A4,A7,PRE_POLY:def 17;
  (divisors b)/.i = HT(p,O) by A4,A7,A8,PARTFUN1:def 6;
  then
A10: (decomp b)/.i = <*HT(p,O), b-'HT(p,O)*> by A9,PRE_POLY:def 17;
  then
A11: (decomp b)/.i = <*HT(p,O), HT(q,O)*> by PRE_POLY:48;
A12: dom s = Seg(len decomp b) by A2,FINSEQ_1:def 3
    .= dom(decomp b) by FINSEQ_1:def 3;
  then
A13: i in dom s by A4,A7,PRE_POLY:def 17;
  reconsider i as Element of NAT by A7;
  consider b1,b2 being bag of n such that
A14: (decomp b)/.i = <*b1, b2*> and
A15: s/.i = p.b1*q.b2 by A3,A13;
A16: b2 = <*HT(p,O), HT(q,O)*>.2 by A11,A14,FINSEQ_1:44
    .= HT(q,O) by FINSEQ_1:44;
A17: now
    let k be Element of NAT;
    assume that
A18: k in dom s and
A19: k <> i;
    consider b1,b2 being bag of n such that
A20: (decomp b)/.k = <*b1, b2*> and
A21: s/.k = p.b1*q.b2 by A3,A18;
    consider b19, b29 being bag of n such that
A22: (decomp b)/.k = <*b19, b29*> and
A23: b = b19+b29 by A12,A18,PRE_POLY:68;
A24: b2 = <*b19, b29*>.2 by A22,A20,FINSEQ_1:44
      .= b29 by FINSEQ_1:44;
A25: b1 = <*b19, b29*>.1 by A22,A20,FINSEQ_1:44
      .= b19 by FINSEQ_1:44;
A26: now
      assume that
A27:  p.b1 <> 0.L and
A28:  q.b2 <> 0.L;
      b1 is Element of Bags n by PRE_POLY:def 12;
      then b1 in Support p by A27,POLYNOM1:def 3;
      then b1 <= HT(p,O),O by Def6;
      then
A29:  [b1,HT(p,O)] in O by Def2;
      b2 is Element of Bags n by PRE_POLY:def 12;
      then b2 in Support q by A28,POLYNOM1:def 3;
      then b2 <= HT(q,O),O by Def6;
      then
A30:  [b2,HT(q,O)] in O by Def2;
A31:  now
        assume b1 = HT(p,O) & b2 = HT(q,O);
        then (decomp b).k = <*HT(p,O), HT(q,O)*> by A12,A18,A20,PARTFUN1:def 6
          .= (decomp b)/.i by A10,PRE_POLY:48
          .= (decomp b).i by A9,PARTFUN1:def 6;
        hence contradiction by A9,A12,A18,A19,FUNCT_1:def 4;
      end;
      now
        per cases by A31;
        case
A32:      b1 <> HT(p,O);
A33:      now
            assume b1+b2 = HT(p,O)+b2;
            then b1 = (HT(p,O)+b2)-'b2 by PRE_POLY:48;
            hence contradiction by A32,PRE_POLY:48;
          end;
A34:      HT(p,O)+b2 is Element of Bags n & HT(p,O)+HT(q,O) is Element of
          Bags n by PRE_POLY:def 12;
          [HT(p,O)+HT(q,O), HT(p,O)+b2] in O & [HT(p,O)+b2, HT(p,O)+HT(q,
          O)] in O by A23,A25,A24,A29,A30,BAGORDER:def 5;
          hence contradiction by A23,A25,A24,A33,A34,ORDERS_1:4;
        end;
        case
A35:      b2 <> HT(q,O);
A36:      now
            assume b2+b1 = HT(q,O)+b1;
            then b2 = (HT(q,O)+b1)-'b1 by PRE_POLY:48;
            hence contradiction by A35,PRE_POLY:48;
          end;
A37:      HT(q,O)+b1 is Element of Bags n & HT(p,O)+HT(q,O) is Element of
          Bags n by PRE_POLY:def 12;
          [HT(p,O)+HT(q,O), HT(q,O)+b1] in O & [HT(q,O)+b1, HT(p,O)+HT(q,
          O)] in O by A23,A25,A24,A29,A30,BAGORDER:def 5;
          hence contradiction by A23,A25,A24,A36,A37,ORDERS_1:4;
        end;
      end;
      hence contradiction;
    end;
    now
      per cases by A26;
      case
        p.b1 = 0.L;
        hence p.b1*q.b2 = 0.L by BINOM:1;
      end;
      case
        q.b2 = 0.L;
        hence p.b1*q.b2 = 0.L by BINOM:2;
      end;
    end;
    hence s/.k = 0.L by A21;
  end;
  b1 = <*HT(p,O), HT(q,O)*>.1 by A11,A14,FINSEQ_1:44
    .= HT(p,O) by FINSEQ_1:44;
  hence thesis by A1,A13,A17,A15,A16,POLYNOM2:3;
end;

theorem Th29:
  for n being Ordinal, T being admissible connected TermOrder of n
  , L being add-associative right_complementable left_zeroed right_zeroed
  well-unital distributive domRing-like non trivial doubleLoopStr, p,q being
  non-zero Polynomial of n,L holds HT(p,T) + HT(q,T) in Support(p*'q)
proof
  let n be Ordinal, O be admissible connected TermOrder of n, L be
  add-associative right_complementable right_zeroed left_zeroed well-unital
  distributive domRing-like non trivial doubleLoopStr, p,q be non-zero
  Polynomial of n,L;
  set b = HT(p,O) + HT(q,O);
  assume
A1: not HT(p,O) + HT(q,O) in Support(p*'q);
  p <> 0_(n,L) by POLYNOM7:def 1;
  then Support p <> {} by POLYNOM7:1;
  then HT(p,O) in Support p by Def6;
  then
A2: p.(HT(p,O)) <> 0.L by POLYNOM1:def 3;
  q <> 0_(n,L) by POLYNOM7:def 1;
  then Support q <> {} by POLYNOM7:1;
  then HT(q,O) in Support q by Def6;
  then
A3: q.(HT(q,O)) <> 0.L by POLYNOM1:def 3;
  b is Element of Bags n by PRE_POLY:def 12;
  then (p*'q).(HT(p,O) + HT(q,O)) = 0.L by A1,POLYNOM1:def 3;
  then p.(HT(p,O)) * q.(HT(q,O)) = 0.L by Lm14;
  hence thesis by A2,A3,VECTSP_2:def 1;
end;

theorem Th30:
  for n being Ordinal, L being add-associative
  right_complementable right_zeroed well-unital distributive non empty
doubleLoopStr, p,q being Polynomial of n,L holds Support(p*'q) c= {s + t where
  s,t is Element of Bags n : s in Support p & t in Support q}
proof
  let n be Ordinal, L be add-associative right_complementable right_zeroed
  well-unital distributive non empty doubleLoopStr, p,q be Polynomial of n,L;
A1: now
    let b be bag of n;
    consider s being FinSequence of L such that
A2: (p*'q).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*q.b2 by POLYNOM1:def 9;
A5: dom s = Seg(len decomp b) by A3,FINSEQ_1:def 3
      .= dom(decomp b) by FINSEQ_1:def 3;
    assume
A6: b in Support(p*'q);
    now
      per cases;
      case
        dom s = {};
        then Seg len s = {} by FINSEQ_1:def 3;
        then len s = 0;
        hence contradiction by A3;
      end;
      case
A7:     dom s <> {};
        set k = the Element of dom s;
        k in dom s by A7;
        then reconsider k as Element of NAT;
        now
          assume
A8:       not( ex k being Element of dom(decomp b), b1,b2 being bag
          of n st (decomp b)/.k = <*b1, b2*> & p.b1 <> 0.L & q.b2 <> 0.L);
A9:       for k being Nat st k in dom s holds s/.k = 0.L
          proof
            let k be Nat;
            assume
A10:        k in dom s;
            then consider b1, b2 being bag of n such that
A11:        (decomp b)/.k = <*b1, b2*> and
A12:        s/.k = p.b1*q.b2 by A4;
            now
              per cases by A5,A8,A10,A11;
              case
                p.b1 = 0.L;
                hence thesis by A12,BINOM:1;
              end;
              case
                q.b2 = 0.L;
                hence thesis by A12,BINOM:2;
              end;
            end;
            hence thesis;
          end;
          then for k9 being Element of NAT st k9 in dom s & k9 <> k holds s/.
          k9 = 0.L;
          then Sum s = s/.k by A7,POLYNOM2:3
            .= 0.L by A7,A9;
          hence contradiction by A6,A2,POLYNOM1:def 3;
        end;
        then consider
        k being Element of dom(decomp b), b1,b2 being bag of n such
        that
A13:    (decomp b)/.k = <*b1, b2*> and
A14:    p.b1 <> 0.L and
A15:    q.b2 <> 0.L;
        k in dom(decomp b) by A5,A7;
        then reconsider k as Element of NAT;
        consider b19, b29 being bag of n such that
A16:    (decomp b)/.k = <*b19, b29*> and
A17:    b = b19+b29 by A5,A7,PRE_POLY:68;
A18:    b29 = <*b1, b2*>.2 by A13,A16,FINSEQ_1:44
          .= b2 by FINSEQ_1:44;
        b2 is Element of Bags n by PRE_POLY:def 12;
        then
A19:    b2 in Support q by A15,POLYNOM1:def 3;
        b1 is Element of Bags n by PRE_POLY:def 12;
        then
A20:    b1 in Support p by A14,POLYNOM1:def 3;
        b19 = <*b1, b2*>.1 by A13,A16,FINSEQ_1:44
          .= b1 by FINSEQ_1:44;
        hence
        ex s,t being bag of n st s in Support p & t in Support q & b = s+
        t by A20,A19,A17,A18;
      end;
    end;
    hence ex s,t being bag of n st s in Support p & t in Support q & b = s+t;
  end;
  now
    let u be set;
    assume
A21: u in Support(p*'q);
    then reconsider u9 = u as Element of Bags n;
    ex s,t being bag of n st s in Support p & t in Support q & u9 = s+t by A1
,A21;
    hence
    u in {s9 + t9 where s9,t9 is Element of Bags n : s9 in Support p & t9
    in Support q};
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th31: :: lemma 5.17 (i), p. 195
  for n being Ordinal, T being admissible connected TermOrder of n
  , L being add-associative right_complementable right_zeroed well-unital
  distributive domRing-like non trivial doubleLoopStr, p,q being non-zero
  Polynomial of n,L holds HT(p*'q,T) = HT(p,T) + HT(q,T)
proof
  let n be Ordinal, O be admissible connected TermOrder of n, L be
  add-associative right_complementable right_zeroed well-unital distributive
  domRing-like non trivial doubleLoopStr, p,q be non-zero Polynomial of n,L;
A1: HT(p,O)+HT(q,O) is Element of Bags n by PRE_POLY:def 12;
  HT(p,O) + HT(q,O) in Support(p*'q) by Th29;
  then HT(p,O) + HT(q,O) <= HT(p*'q,O),O by Def6;
  then
A2: [HT(p,O) + HT(q,O),HT(p*'q,O)] in O by Def2;
  Support p*'q <> {} by Th29;
  then
A3: HT(p*'q,O) in Support(p*'q) by Def6;
  Support(p*'q) c= {s + t where s,t is Element of Bags n : s in Support p
  & t in Support q} by Th30;
  then
  HT(p*'q,O) in {s + t where s,t is Element of Bags n : s in Support p & t
  in Support q} by A3;
  then consider s,t being Element of Bags n such that
A4: HT(p*'q,O) = s + t and
A5: s in Support p and
A6: t in Support q;
  s <= HT(p,O),O by A5,Def6;
  then [s,HT(p,O)] in O by Def2;
  then
A7: [s + t,HT(p,O) + t] in O by BAGORDER:def 5;
  t <= HT(q,O),O by A6,Def6;
  then [t,HT(q,O)] in O by Def2;
  then
A8: [t + HT(p,O), HT(p,O)+HT(q,O)] in O by BAGORDER:def 5;
  s + t is Element of Bags n & HT(p,O) + t is Element of Bags n by
PRE_POLY:def 12;
  then [s + t,HT(p,O)+HT(q,O)] in O by A1,A7,A8,ORDERS_1:5;
  hence thesis by A2,A4,A1,ORDERS_1:4;
end;

theorem Th32: :: lemma 5.17 (iii), p. 195
  for n being Ordinal, T being admissible connected TermOrder of n
  , L being add-associative right_complementable right_zeroed well-unital
  distributive domRing-like non trivial doubleLoopStr, p,q being non-zero
  Polynomial of n,L holds HC(p*'q,T) = HC(p,T) * HC(q,T)
proof
  let n be Ordinal, O being admissible connected TermOrder of n, L be
  add-associative right_complementable right_zeroed well-unital distributive
  domRing-like non trivial doubleLoopStr, p,q be non-zero Polynomial of n,L;
  thus HC(p*'q,O) = (p*'q).(HT(p,O) + HT(q,O)) by Th31
    .= HC(p,O) * HC(q,O) by Lm14;
end;

theorem :: lemma 5.17 (ii), p. 195
  for n being Ordinal, T being admissible connected TermOrder of n, L
  being add-associative right_complementable right_zeroed well-unital
  distributive domRing-like non trivial doubleLoopStr, p,q being non-zero
  Polynomial of n,L holds HM(p*'q,T) = HM(p,T) *' HM(q,T)
proof
  let n be Ordinal, O being admissible connected TermOrder of n, L be
  add-associative right_complementable right_zeroed well-unital distributive
  domRing-like non trivial doubleLoopStr, p,q be non-zero Polynomial of n,L;
  thus HM(p*'q,O) = Monom(HC(p,O) * HC(q,O),HT(p*'q,O)) by Th32
    .= Monom(HC(p,O) * HC(q,O),HT(p,O) + HT(q,O)) by Th31
    .= HM(p,O) *' HM(q,O) by Th3;
end;

theorem :: lemma 5.17 (iv), p. 195
  for n being Ordinal, T being admissible connected TermOrder of n, L
being right_zeroed non empty addLoopStr, p,q being Polynomial of n,L holds HT
  (p+q,T) <= max(HT(p,T),HT(q,T),T), T
proof
  let n be Ordinal, O being admissible connected TermOrder of n, L be
  right_zeroed non empty addLoopStr, p,q be Polynomial of n,L;
  per cases;
  suppose
A1: HT(p+q,O) in Support(p+q);
A2: Support(p+q) c= Support p \/ Support q by POLYNOM1:20;
    now
      per cases by A1,A2,XBOOLE_0:def 3;
      case
A3:     HT(p+q,O) in Support(p);
        then
A4:     HT(p+q,O) <= HT(p,O),O by Def6;
        now
          per cases by Th12;
          case
            max(HT(p,O),HT(q,O),O) = HT(p,O);
            hence thesis by A3,Def6;
          end;
          case
A5:         max(HT(p,O),HT(q,O),O) = HT(q,O);
            then HT(p,O) <= HT(q,O),O by Th14;
            hence thesis by A4,A5,Th8;
          end;
        end;
        hence thesis;
      end;
      case
A6:     HT(p+q,O) in Support(q);
        then
A7:     HT(p+q,O) <= HT(q,O),O by Def6;
        now
          per cases by Th12;
          case
            max(HT(p,O),HT(q,O),O) = HT(q,O);
            hence thesis by A6,Def6;
          end;
          case
A8:         max(HT(p,O),HT(q,O),O) = HT(p,O);
            then HT(q,O) <= HT(p,O),O by Th14;
            hence thesis by A7,A8,Th8;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  suppose
    not HT(p+q,O) in Support(p+q);
    then HT(p+q,O) = EmptyBag n by Def6;
    then [HT(p+q,O),max(HT(p,O),HT(q,O),O)] in O by BAGORDER:def 5;
    hence thesis by Def2;
  end;
end;

begin :: Reductum

definition
  let n be Ordinal, T be connected TermOrder of n, L be add-associative
right_complementable right_zeroed non empty addLoopStr, p be Polynomial of n,
  L;
  func Red(p,T) -> Polynomial of n,L equals
  p - HM(p,T);
  coherence;
end;

Lm15: for n being Ordinal, O being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, p
being Polynomial of n,L holds not(HT(p,O) in Support(Red(p,O)))
proof
  let n being Ordinal, O being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed non trivial addLoopStr, p
  being Polynomial of n,L;
  assume HT(p,O) in Support(Red(p,O));
  then (Red(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 3;
  then (p + -HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 6;
  then p.(HT(p,O)) + (-HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:15;
  then
A1: p.(HT(p,O)) + -HM(p,O).(HT(p,O)) <> 0.L by POLYNOM1:17;
  HM(p,O).(HT(p,O)) = p.(HT(p,O)) by Lm8;
  hence thesis by A1,RLVECT_1:def 10;
end;

Lm16: for n being Ordinal, O 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 st b in Support p & b <> HT(p,O)
holds b in Support(Red(p,O))
proof
  let n being Ordinal, O 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;
  assume that
A1: b in Support p and
A2: b <> HT(p,O);
  (Red(p,O)).b = (p + -HM(p,O)).b by POLYNOM1:def 6
    .= p.b + (-HM(p,O)).b by POLYNOM1:15
    .= p.b + -HM(p,O).b by POLYNOM1:17
    .= p.b + - 0.L by A2,Th19
    .= p.b + 0.L by RLVECT_1:12
    .= p.b by RLVECT_1:4;
  then b is Element of Bags n & (Red(p,O)).b <> 0.L by A1,POLYNOM1:def 3
;
  hence thesis by POLYNOM1:def 3;
end;

Lm17: for n being Ordinal, O being connected TermOrder of n, L being
add-associative right_complementable right_zeroed non trivial addLoopStr, p
being Polynomial of n,L holds Support(Red(p,O)) = Support(p) \ {HT(p,O)}
proof
  let n being Ordinal, O being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed non trivial addLoopStr, p
  being Polynomial of n,L;
A1: now
    let u be set;
    assume
A2: u in Support(Red(p,O));
    then reconsider u9 = u as Element of Bags n;
    reconsider u9 as bag of n;
A3: (p - HM(p,O)).u9 <> 0.L by A2,POLYNOM1:def 3;
A4: not u9 = HT(p,O) by A2,Lm15;
    (p + -HM(p,O)).u9 = p.u9 + (-HM(p,O)).u9 by POLYNOM1:15
      .= p.u9 + -HM(p,O).u9 by POLYNOM1:17;
    then (p + -HM(p,O)).u9 = p.u9 + - 0.L by A4,Th19
      .= p.u9 + 0.L by RLVECT_1:12
      .= p.u9 by RLVECT_1:4;
    then p.u9 <> 0.L by A3,POLYNOM1:def 6;
    then
A5: u9 in Support p by POLYNOM1:def 3;
    not u9 in {HT(p,O)} by A4,TARSKI:def 1;
    hence u in Support(p) \ {HT(p,O)} by A5,XBOOLE_0:def 5;
  end;
  now
    let u be set;
    assume
A6: u in Support(p) \ {HT(p,O)};
    then reconsider u9 = u as Element of Bags n;
    reconsider u9 as bag of n;
    not u in {HT(p,O)} by A6,XBOOLE_0:def 5;
    then
A7: u9 <> HT(p,O) by TARSKI:def 1;
    u in Support p by A6,XBOOLE_0:def 5;
    hence u in Support(Red(p,O)) by A7,Lm16;
  end;
  hence thesis by A1,TARSKI:1;
end;

theorem
  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 Support(Red(p,T)) c= Support(p)
proof
  let n being Ordinal, O being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed non trivial addLoopStr, p
  being Polynomial of n,L;
  Support(Red(p,O)) = Support(p) \ {HT(p,O)} by Lm17;
  hence thesis by XBOOLE_1:36;
end;

theorem
  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 Support(Red(p,T)) = Support(p) \ {HT(p,T)} by
Lm17;

Lm18: 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 (Red(p,T)).(HT(p,T)) = 0.L
proof
  let n be Ordinal, O being connected TermOrder of n, L be add-associative
right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of
  n,L;
  HT(p,O) in {HT(p,O)} & Support(Red(p,O)) = Support(p) \ {HT(p,O)} by Lm17,
TARSKI:def 1;
  then not HT(p,O) in Support(Red(p,O)) by XBOOLE_0:def 5;
  hence thesis by POLYNOM1:def 3;
end;

Lm19: for n being Ordinal, O 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 st b <> HT(p,O) holds (Red(p,O)).b =
p.b
proof
  let n be Ordinal, O being 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 b <> HT(p,O);
  then not b in {HT(p,O)} by TARSKI:def 1;
  then
A2: not b in Support(HM(p,O)) by Lm12;
  thus (Red(p,O)).b = (p + -HM(p,O)).b by POLYNOM1:def 6
    .= p.b + (-HM(p,O)).b by POLYNOM1:15
    .= p.b + -(HM(p,O)).b by POLYNOM1:17
    .= p.b + -0.L by A2,A1,POLYNOM1:def 3
    .= p.b + 0.L by RLVECT_1:12
    .= p.b by RLVECT_1:4;
end;

theorem
  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 Support(HM(p,T) + Red(p,T)) = Support p
proof
  let n being Ordinal, O being connected TermOrder of n, L being
  add-associative right_complementable right_zeroed non trivial addLoopStr, p
  being Polynomial of n,L;
A1: now
    let u be set;
    assume
A2: u in Support p;
    then reconsider u9 = u as Element of Bags n;
    reconsider u9 as bag of n;
A3: p.u9 <> 0.L by A2,POLYNOM1:def 3;
    now
      per cases;
      case
A4:     u9 = HT(p,O);
        then
A5:     p.(HT(p,O)) <> 0.L by A2,POLYNOM1:def 3;
        (HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
          .= HM(p,O).u9 + 0.L by A4,Lm18
          .= HM(p,O).u9 by RLVECT_1:4
          .= HC(p,O) by A4,Lm8;
        hence u9 in Support(HM(p,O) + Red(p,O)) by A5,POLYNOM1:def 3;
      end;
      case
A6:     u9 <> HT(p,O);
        (HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
          .= HM(p,O).u9 + p.u9 by A6,Lm19
          .= 0.L + p.u9 by A6,Th19
          .= p.u9 by RLVECT_1:4;
        hence u9 in Support(HM(p,O) + Red(p,O)) by A3,POLYNOM1:def 3;
      end;
    end;
    hence u in Support(HM(p,O) + Red(p,O));
  end;
  now
    let u be set;
    assume
A7: u in Support(HM(p,O) + Red(p,O));
    then reconsider u9 = u as Element of Bags n;
    reconsider u9 as bag of n;
A8: (HM(p,O) + Red(p,O)).u9 <> 0.L by A7,POLYNOM1:def 3;
    now
      per cases;
      case
A9:     u9 = HT(p,O);
        (HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
          .= HM(p,O).HT(p,O) + 0.L by A9,Lm18
          .= HM(p,O).HT(p,O) by RLVECT_1:4
          .= p.u9 by A9,Lm8;
        hence u9 in Support p by A8,POLYNOM1:def 3;
      end;
      case
A10:    u9 <> HT(p,O);
        (HM(p,O) + Red(p,O)).u9 = HM(p,O).u9 + Red(p,O).u9 by POLYNOM1:15
          .= 0.L + Red(p,O).u9 by A10,Th19
          .= Red(p,O).u9 by RLVECT_1:4
          .= p.u by A10,Lm19;
        hence u9 in Support p by A8,POLYNOM1:def 3;
      end;
    end;
    hence u in Support p;
  end;
  hence thesis by A1,TARSKI:1;
end;

theorem
  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) + Red(p,T) = p
proof
  let n be Ordinal, O being connected TermOrder of n, L be add-associative
right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of
  n,L;
A1: now
    let x be set;
    assume x in Bags n;
    then reconsider x9 = x as Element of Bags n;
    now
      per cases;
      case
A2:     x = HT(p,O);
        hence (HM(p,O) + Red(p,O)).x = HM(p,O).HT(p,O) + Red(p,O).HT(p,O) by
POLYNOM1:15
          .= HM(p,O).HT(p,O) + 0.L by Lm18
          .= HM(p,O).HT(p,O) by RLVECT_1:4
          .= p.x by A2,Lm8;
      end;
      case
A3:     x <> HT(p,O);
        (HM(p,O) + Red(p,O)).x9 = HM(p,O).x9 + Red(p,O).x9 by POLYNOM1:15
          .= HM(p,O).x9 + p.x9 by A3,Lm19
          .= 0.L + p.x9 by A3,Th19
          .= p.x9 by RLVECT_1:4;
        hence p.x = (HM(p,O) + Red(p,O)).x;
      end;
    end;
    hence p.x = (HM(p,O) + Red(p,O)).x;
  end;
  dom p = Bags n & dom(HM(p,O) + Red(p,O)) = Bags n by FUNCT_2:def 1;
  hence thesis by A1,FUNCT_1:2;
end;

theorem
  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 (Red(p,T)).(HT(p,T)) = 0.L by Lm18;

theorem
  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 st b in Support p & b <> HT(p,T)
  holds (Red(p,T)).b = p.b by Lm19;