The Mizar article:

Term Orders

by
Christoph Schwarzweller

Received December 20, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: TERMORD
[ MML identifier index ]


environ

 vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, TRIANG_1, FINSEQ_1, VECTSP_1,
      RLVECT_1, ORDINAL1, LATTICES, ALGSEQ_1, ANPROJ_1, CAT_3, GROUP_1,
      VECTSP_2, RELAT_1, RELAT_2, REALSET1, ALGSTR_1, CARD_1, ARYTM_1, MCART_1,
      FINSEQ_4, ARYTM_3, SQUARE_1, PBOOLE, ORDERS_1, ORDERS_2, FINSET_1,
      BAGORDER, WELLORD1, DICKSON, TERMORD;
 notation NUMBERS, XCMPLX_0, XREAL_0, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0,
      RELAT_1, MONOID_0, CARD_1, BAGORDER, RELSET_1, FUNCT_1, FINSET_1,
      ORDINAL1, NAT_1, ALGSTR_1, RLVECT_1, PBOOLE, FINSEQ_1, MCART_1, TRIANG_1,
      REALSET1, VECTSP_1, VECTSP_2, RELAT_2, POLYNOM1, BINARITH, ORDERS_1,
      ORDERS_2, FINSEQ_4, WELLORD1, POLYNOM7;
 constructors ALGSTR_2, POLYNOM7, MONOID_0, BINOM, BAGORDER, MCART_1, TRIANG_1,
      ORDERS_2, MEMBERED;
 clusters XREAL_0, STRUCT_0, FINSET_1, RELSET_1, FINSEQ_1, CARD_1, ALGSTR_1,
      POLYNOM1, POLYNOM2, POLYNOM7, BAGORDER, VECTSP_1, NAT_1, MEMBERED,
      NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, RELAT_1, POLYNOM1, PBOOLE, NAT_1,
      REAL_1, FINSEQ_4, BINOM, TRIANG_1, RLVECT_1, VECTSP_2, FINSET_1,
      POLYNOM7, POLYNOM2, NAT_2, RELAT_2, CARD_1, CARD_2, ORDERS_1, MATRLIN,
      SEQM_3, XBOOLE_0, XBOOLE_1, BINARITH, ORDERS_2, MCART_1, BAGORDER,
      WELLORD1, VECTSP_1, XCMPLX_0, XCMPLX_1;
 schemes BINOM;

begin :: Preliminaries

definition
cluster non trivial LoopStr;
existence
 proof
 consider R being Field;
 take R;
 thus thesis;
 end;
end;

definition
cluster add-associative right_complementable right_zeroed
        (non trivial LoopStr);
existence
 proof
 consider F being Field;
 take F;
 thus thesis;
 end;
end;

definition
let X be set,
    b be bag of X;
attr b is non-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,POLYNOM1:def 13;
      then b1.k - b1.k <= b2.k - b1.k by REAL_1:49;
      hence 0 <= b2.k - b1.k by XCMPLX_1:14;
      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;
   case n <> {};
     then reconsider n' = n as non empty set;
     set b = { [k,b2.k -' b1.k] where k is Element of n' : not contradiction};
     A4: now let x be set;
        assume x in b;
        then consider k being Element of n' such that
        A5: x = [k,b2.k -' b1.k];
        thus ex y,z being set st x = [y,z] by A5;
        end;
       now let x,y1,y2 be set;
        assume A6: [x,y1] in b & [x,y2] in b;
        then consider k being Element of n' such that
        A7: [x,y1] = [k,b2.k -' b1.k];
        consider k' being Element of n' such that
        A8: [x,y2] = [k',b2.k' -' b1.k'] by A6;
          k = [x,y1]`1 by A7,MCART_1:def 1
             .= x by MCART_1:def 1
             .= [x,y2]`1 by MCART_1:def 1
             .= k' by A8,MCART_1:def 1;
        hence y1 = [x,y2]`2 by A7,A8,MCART_1:def 2
               .= y2 by MCART_1:def 2;
        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 RELAT_1:def 4;
         consider k being Element of n' such that
         A11: [x,y] = [k,b2.k -' b1.k] by A10;
           x = [k,b2.k -' b1.k]`1 by A11,MCART_1:def 1 .= k by MCART_1:def 1;
         hence x in n';
         end;
       now let x be set;
         assume x in n';
         then reconsider k = x as Element of n';
           [k,b2.k -' b1.k] in b;
         hence x in dom b by RELAT_1:def 4;
         end;
     then A12: dom b = n' by A9,TARSKI:2;
     then reconsider b as ManySortedSet of n' by PBOOLE:def 3;
       now let x be set;
        assume x in rng b;
        then consider y be set such that
        A13: [y,x] in b by RELAT_1:def 5;
        consider k being Element of n' such that
        A14: [y,x] = [k,b2.k -' b1.k] by A13;
          x = [k,b2.k -' b1.k]`2 by A14,MCART_1:def 2
         .= b2.k -' b1.k by MCART_1:def 2;
        hence x in NAT;
        end;
     then A15: rng b c= NAT by TARSKI:def 3;
     A16: now let k be set;
        assume k in n;
        then consider u being set such that
        A17: [k,u] in b by A12,RELAT_1:def 4;
        consider k' being Element of n' such that
        A18: [k,u] = [k',b2.k' -' b1.k'] by A17;
        A19: k = [k',b2.k' -' b1.k']`1 by A18,MCART_1:def 1
             .= k' by MCART_1:def 1;
          u = [k',b2.k' -' b1.k']`2 by A18,MCART_1:def 2
         .= b2.k' -' b1.k' by MCART_1:def 2;
        hence b.k = b2.k -' b1.k by A17,A19,FUNCT_1:8;
        end;
       now let x be set;
        assume A20: x in support b;
        then A21: b.x <> 0 by POLYNOM1:def 7;
        A22: support b c= dom b by POLYNOM1:41;
          now assume not(x in support b2);
          then A23: b2.x = 0 by POLYNOM1:def 7;
            0 <= b1.x by NAT_1:18;
          then 0 = b2.x-'b1.x by A23,NAT_2:10;
          hence contradiction by A12,A16,A20,A21,A22;
          end;
        hence x in support b2;
        end;
     then support b c= support b2 by TARSKI:def 3;
     then support b is finite by FINSET_1:13;
     then reconsider b as bag of n by A15,POLYNOM1:def 8,SEQM_3:def 8;
     take b;
       now let k be set;
       assume A24: k in n;
       A25: 0 <= b2.k - b1.k by A2;
       thus b1.k + b.k
               = b1.k + (b2.k -' b1.k) by A16,A24
              .= b1.k + (b2.k - b1.k) by A25,BINARITH:def 3
              .= b1.k + (b2.k + -b1.k) by XCMPLX_0:def 8
              .= (b1.k + - b1.k) + b2.k by XCMPLX_1:1
              .= (b1.k - b1.k) + b2.k by XCMPLX_0:def 8
              .= 0 + b2.k by XCMPLX_1:14
              .= b2.k;
       end;
     then b2 = b1 + b by POLYNOM1:37;
     hence ex b being bag of n st b2 = b1 + b;
     end;
   hence ex b being bag of n st b2 = b1 + b;
   end;
hence thesis by POLYNOM1:54;
end;

theorem Th2:
for n being Ordinal,
    L being add-associative right_complementable right_zeroed
            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
         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 the carrier of L such that
  A1: (Z*'p).b = Sum s and len s = len decomp b and
  A2: for k being 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 26;
    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:81 .= 0.L by VECTSP_1:39;
    end;
  then Sum s = 0.L by MATRLIN:15;
  hence (Z*'p).b = Z.b by A1,POLYNOM1:81;
  end;
hence 0_(n,L)*'p = 0_(n,L) by FUNCT_2:113;
end;

definition
let n be Ordinal,
    L be add-associative right_complementable right_zeroed
         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;
 suppose A1: Support(m1*'m2) <> {};
     now per cases;
   case A2: Support(m1) <> {} & Support(m2) <> {};
   then consider mb1 being bag of n such that
   A3: Support(m1) = {mb1} by POLYNOM7:6;
     mb1 in Support m1 by A3,TARSKI:def 1;
   then A4: m1.mb1 <> 0.L by POLYNOM1:def 9;
   A5: now let b be bag of n;
        assume A6: b <> mb1;
        consider b' being bag of n such that
        A7: for b being bag of n st b <> b' holds m1.b = 0.L
            by POLYNOM7:def 4;
          b' = mb1 by A4,A7;
        hence m1.b = 0.L by A6,A7;
        end;
   consider mb2 being bag of n such that
   A8: Support(m2) = {mb2} by A2,POLYNOM7:6;
     mb2 in Support m2 by A8,TARSKI:def 1;
   then A9: m2.mb2 <> 0.L by POLYNOM1:def 9;
   A10: now let b be bag of n;
        assume A11: b <> mb2;
        consider b' being bag of n such that
        A12: for b being bag of n st b <> b' holds m2.b = 0.L
            by POLYNOM7:def 4;
          b' = mb2 by A9,A12;
        hence m2.b = 0.L by A11,A12;
        end;
   consider b being 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 the carrier of L such that
   A14: (m1*'m2).b = Sum s &
       len s = len decomp b &
       for k being 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 26;
   A15: dom s = Seg(len decomp b) by A14,FINSEQ_1:def 3
            .= dom(decomp b) by FINSEQ_1:def 3;
   A16: now assume A17: b <> mb1 + mb2;
       A18: now let k be Nat;
            assume A19: k in dom s;
            then consider b1,b2 being bag of n such that
            A20: (decomp b)/.k = <*b1, b2*> & s/.k = m1.b1*m2.b2 by A14;
            consider b1',b2' being bag of n such that
            A21: (decomp b)/.k = <*b1',b2'*> & b = b1'+b2'
                by A15,A19,POLYNOM1:72;
            A22: b1 = <*b1', b2'*>.1 by A20,A21,FINSEQ_1:61
               .= b1' by FINSEQ_1:61;
            A23: b2 = <*b1', b2'*>.2 by A20,A21,FINSEQ_1:61
              .= b2' by FINSEQ_1:61;
              now per cases by A17,A21,A22,A23;
            case b1 <> mb1;
              then m1.b1 = 0.L by A5;
              hence m1.b1*m2.b2 = 0.L by BINOM:1;
            case b2 <> mb2;
              then m2.b2 = 0.L by A10;
              hence m1.b1*m2.b2 = 0.L by BINOM:2;
            end;
            hence s/.k = 0.L by A20;
            end;
         now per cases;
       case dom s = {};
         then s = <*>(the carrier of L) by FINSEQ_1:26;
         hence (m1*'m2).b = 0.L by A14,RLVECT_1:60;
       case A24: dom s <> {};
         consider k being Element of dom s;
         A25: k in dom s by A24;
           for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L by A18;
         then s/.k = (m1*'m2).b by A14,A25,POLYNOM2:5;
         hence (m1*'m2).b = 0.L by A18,A25;
       end;
       hence contradiction by A13,POLYNOM1:def 9;
       end;
     now let b' be bag of n;
     assume A26: b' <> b;
     consider s being FinSequence of the carrier of L such that
     A27: (m1*'m2).b' = Sum s &
         len s = len decomp b' &
         for k being 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 26;
     A28: dom s = Seg(len decomp b') by A27,FINSEQ_1:def 3
              .= dom(decomp b') by FINSEQ_1:def 3;
     A29: now let k be Nat;
         assume A30: k in dom s;
         then consider b1, b2 being bag of n such that
         A31: (decomp b')/.k = <*b1,b2*> & s/.k = m1.b1*m2.b2 by A27;
         consider b1',b2' being bag of n such that
         A32: (decomp b')/.k = <*b1',b2'*> & b' = b1'+b2' by A28,A30,POLYNOM1:
72;
         A33: b1 = <*b1', b2'*>.1 by A31,A32,FINSEQ_1:61
               .= b1' by FINSEQ_1:61;
         A34: b2 = <*b1', b2'*>.2 by A31,A32,FINSEQ_1:61
               .= b2' by FINSEQ_1:61;
           now per cases by A16,A26,A32,A33,A34;
         case b1 <> mb1;
           then m1.b1 = 0.L by A5;
           hence m1.b1*m2.b2 = 0.L by BINOM:1;
         case b2 <> mb2;
           then m2.b2 = 0.L by A10;
           hence m1.b1*m2.b2 = 0.L by BINOM:2;
         end;
         hence s/.k = 0.L by A31;
         end;
       now per cases;
     case dom s = {};
       then s = <*>(the carrier of L) by FINSEQ_1:26;
       hence (m1*'m2).b' = 0.L by A27,RLVECT_1:60;
     case A35: dom s <> {};
       consider k being Element of dom s;
       A36: k in dom s by A35;
         for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L by A29;
       then s/.k = (m1*'m2).b' by A27,A36,POLYNOM2:5;
       hence (m1*'m2).b' = 0.L by A29,A36;
      end;
     hence (m1*'m2).b' = 0.L;
     end;
   hence thesis by POLYNOM7:def 4;
   case A37: Support(m1) = {} or Support(m2) = {};
     now per cases by A37;
   case Support(m1) = {};
     then m1 = 0_(n,L) by POLYNOM7:1;
     hence thesis by Th2;
   case Support(m2) = {};
     then m2 = 0_(n,L) by POLYNOM7:1;
     hence thesis by POLYNOM1:87;
   end;
   hence thesis;
   end;
 hence thesis;
 end;
end;

definition
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 the carrier of L such that
   A2: p.b = Sum s &
      len s = len decomp b &
      for k being 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 26;

   A3: dom s = Seg(len decomp b) by A2,FINSEQ_1:def 3
            .= dom(decomp b) by FINSEQ_1:def 3;
   A4: now let k be Nat;
       assume A5: k in dom s;
       then consider b1, b2 being bag of n such that
       A6: (decomp b)/.k = <*b1,b2*> & s/.k = c1.b1*c2.b2 by A2;
       consider b1',b2' being bag of n such that
       A7: (decomp b)/.k = <*b1',b2'*> & b = b1'+b2' by A3,A5,POLYNOM1:72;
       A8: b1 = <*b1', b2'*>.1 by A6,A7,FINSEQ_1:61
             .= b1' by FINSEQ_1:61;
         b2 = <*b1', b2'*>.2 by A6,A7,FINSEQ_1:61
         .= b2' by FINSEQ_1:61;
       then A9: b1 <> EmptyBag n or b2 <> EmptyBag n by A1,A7,A8,POLYNOM1:57;
         now per cases by A9,POLYNOM7:def 8;
       case c1.b1 = 0.L;
         hence s/.k = 0.L by A6,BINOM:1;
       case c2.b2 = 0.L;
         hence s/.k = 0.L by A6,BINOM:2;
       end;
       hence s/.k = 0.L;
       end;
     now per cases;
   case dom s = {};
     then s = <*>(the carrier of L) by FINSEQ_1:26;
     hence p.b = 0.L by A2,RLVECT_1:60;
   case A10: dom s <> {};
     consider k being Element of dom s;
     A11: k in dom s by A10;
       for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L by A4;
     then Sum s = s/.k by A11,POLYNOM2:5;
     hence p.b = 0.L by A2,A4,A11;
   end;
   hence p.b = 0.L;
   end;
 hence thesis by POLYNOM7:def 8;
 end;
end;

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

theorem
  for n being Ordinal,
    L being add-associative right_complementable right_zeroed
            unital distributive domRing-like (non trivial doubleLoopStr),
    a,a' being Element of L
holds (a * a') _(n,L) = (a _(n,L)) *' (a' _(n,L))
proof
let n be Ordinal,
    L be add-associative right_complementable right_zeroed
         unital distributive domRing-like (non trivial doubleLoopStr),
    a,a' be Element of L;
per cases;
suppose A1: a is non-zero & a' is non-zero;
    term((a*a') _(n,L)) = EmptyBag n & coefficient((a*a') _(n,L)) = a*a'
     by POLYNOM7:23;
  then A2: (a * a') _(n,L) = Monom(a*a',EmptyBag n) by POLYNOM7:11;
    term(a _(n,L)) = EmptyBag n & coefficient(a _(n,L)) = a
     by POLYNOM7:23;
  then A3: a _(n,L) = Monom(a,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 POLYNOM1:57;
  hence thesis by A1,A2,A3,A4,Th3;
suppose A5: not(a is non-zero & a' is non-zero);
    now per cases by A5,RLVECT_1:def 13;
  case A6: a = 0.L;
    then a * a' = 0.L by BINOM:1;
    then A7: (a * a') _(n,L) = 0_(n,L) by POLYNOM7:19;
      a _(n,L) = 0_(n,L) by A6,POLYNOM7:19;
    hence thesis by A7,Th2;
  case A8: a' = 0.L;
    then a * a' = 0.L by BINOM:2;
    then A9: (a * a') _(n,L) = 0_(n,L) by POLYNOM7:19;
      a' _(n,L) = 0_(n,L) by A8,POLYNOM7:19;
    hence thesis by A9,POLYNOM1:87;
  end;
  hence thesis;
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 2;
suppose b in dom T;
  then b is Element of Bags n;
  hence thesis;
suppose b in rng T;
  then b is Element of Bags n;
  hence thesis;
end;

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

definition
::: theorem 5.5 (ii), p. 190
let n be Nat;
cluster -> well_founded (admissible TermOrder of n);
coherence
 proof
 let T be admissible TermOrder of n;
   T is well-ordering by BAGORDER:35;
 hence thesis by WELLORD1:def 4;
 end;
end;

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

definition
let n be Ordinal,
    T be TermOrder of n,
    b,b' be bag of n;
pred b < b',T means :Def3:
  b <= b',T & b <> b';
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:97;
  then
A1: T is_reflexive_in Bags n by RELAT_2:def 9;
  b is Element of Bags n by POLYNOM1:def 14;
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;
assume b1 <= b2,T & b2 <= b1,T;
then A1: [b1,b2] in T & [b2,b1] in T by Def2;
  field T = Bags n by ORDERS_1:97;
  then
A2: T is_antisymmetric_in Bags n by RELAT_2:def 12;
  b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14;
hence thesis by A1,A2,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:97;
  then
A1: T is_reflexive_in Bags n by RELAT_2:def 9;
  b is Element of Bags n by POLYNOM1:def 14;
then [b,b] in T by A1,RELAT_2:def 1;
hence thesis by RELAT_1:30;
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;
suppose A2: b1 <> b2;
A3: b1 <= b2,T implies not(b2 < b1,T)
   proof
   assume A4: b1 <= b2,T;
   assume b2 < b1,T;
   then b2 <= b1,T & b1 <> b2 by Def3;
   hence thesis by A4,Lm3;
   end;
  not(b2 < b1,T) implies b1 <= b2,T
   proof
   assume A5: not(b2 < b1,T);
     now per cases by A5,Def3;
   case not(b2 <= b1,T);
     then A6: not([b2,b1] in T) by Def2;
       b1 in field T & b2 in field T by Lm4;
     then [b1,b2] in T by A1,A2,A6,RELAT_2:def 6;
     hence thesis by Def2;
   case b1 = b2;
     hence thesis by A2;
   end;
   hence thesis;
   end;
hence thesis by A3;
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:97;
  then
   A3: T is_reflexive_in Bags n by RELAT_2:def 9;
     b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14;
   then [b1,b2] in T by A2,A3,RELAT_2:def 1;
   hence thesis by Def2;
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;

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;
assume b1 <= b2,T & b2 <= b3,T;
then A1: [b1,b2] in T & [b2,b3] in T by Def2;
  field T = Bags n by ORDERS_1:97;
  then
A2: T is_transitive_in Bags n by RELAT_2:def 16;
  b1 is Element of Bags n & b2 is Element of Bags n &
b3 is Element of Bags n by POLYNOM1:def 14;
then [b1,b3] in T by A1,A2,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 7;
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 7;
then [b1,b2] in T by POLYNOM1:57;
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 min(b1,b2,T) = b2 by Def4;
case b1 = b2;
  then b1 <= b2,T by Lm2;
  hence contradiction by A1,Def4;
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 max(b1,b2,T) = b2 by Def5;
case b1 = b2;
  then b2 <= b1,T by Lm2;
  hence contradiction by A1,Def5;
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;
A1: b <= b,T by Lm2;
hence min(b,b,T) = b by Def4;
thus max(b,b,T) = b by A1,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;
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;
  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;
  hence thesis;
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;
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;
  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;
  hence thesis;
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);
    case b1 <> b2;
      then not(b2 <= b1,T) by A2,Lm3;
      hence min(b2,b1,T) = min(b1,b2,T) by A1,Def4;
    end;
    hence min(b1,b2,T) = min(b2,b1,T);
  case b1 = b2;
    hence min(b2,b1,T) = min(b1,b2,T);
  end;
  hence min(b1,b2,T) = min(b2,b1,T);
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;
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);
    case b1 <> b2;
      then not(b1 <= b2,T) by A6,Lm3;
      hence max(b2,b1,T) = max(b1,b2,T) by A5,Def5;
    end;
    hence max(b1,b2,T) = max(b2,b1,T);
  case b1 = b2;
    hence max(b2,b1,T) = max(b1,b2,T);
  end;
  hence max(b1,b2,T) = max(b2,b1,T);
case A7: max(b1,b2,T) <> b1;
    now
      now per cases by Lm5;
    case b1 <= b2,T;
      hence max(b2,b1,T) = b2 by Def5 .= max(b1,b2,T) by A7,Th12;
    case b2 <= b1,T;
      hence max(b2,b1,T) = max(b1,b2,T) by A7,Def5;
    end;
    hence max(b2,b1,T) = max(b1,b2,T);
  end;
  hence max(b2,b1,T) = max(b1,b2,T);
  end;
hence max(b1,b2,T) = max(b2,b1,T);
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: min(b1,b2,T) = b1;
     now per cases by A2,Def4;
   case b1 <= b2,T;
     then max(b2,b1,T) = b2 by Def5;
     hence max(b1,b2,T) = b2 by Th15;
   case b1 = b2;
     hence max(b1,b2,T) = b2 by Th12;
   end;
   hence max(b1,b2,T) = b2;
   end;
  now assume A3: max(b1,b2,T) = b2;
     now per cases by A3,Def5;
   case not(b2 <= b1,T);
     then b1 <= b2,T by Lm5;
     hence min(b1,b2,T) = b1 by Def4;
   case b1 = b2;
     hence min(b1,b2,T) = b1 by Th11;
   end;
   hence min(b1,b2,T) = b1;
   end;
hence thesis by A1;
end;

begin :: Headterms, Headmonomials and Headcoefficients

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 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;
suppose A1: Support p <> {};
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 b being bag of n st b in B holds [b,b'] in O;
A2: P[1]
   proof let B be finite Subset of Bags n;
    assume A3: card B = 1;
    consider x being set;
      card {x} = card B by A3,CARD_1:79;
    then consider b being set such that
    A4: B = {b} by CARD_1:49;
    A5: b in B by A4,TARSKI:def 1;
    then reconsider b as Element of Bags n;
    reconsider b as bag of n;
      now let b' be bag of n;
      assume b' in B;
      then b' = b by A4,TARSKI:def 1;
      hence [b',b] in O by ORDERS_1:12;
      end;
    hence ex b' being bag of n st
          b' in B &
          for b being bag of n st b in B holds [b,b'] in O
      by A5;
    end;
A6: for k being Nat st 1 <= k holds P[k] implies P[k+1]
    proof
    let k be Nat;
    assume A7: 1 <= k;
    thus P[k] implies P[k+1]
       proof
       assume A8: P[k];
       thus P[k+1]
         proof
         let B be finite Subset of Bags n;
         assume A9: card B = k+1;
         then reconsider B as non empty finite Subset of Bags n by CARD_1:47;
         consider x being Element of B;
           x in B & B c= Bags n;
         then reconsider x as Element of Bags n;
         reconsider x as bag of n;
         set X = B \ {x};
         A10: x in X iff x in B & not x in {x} by XBOOLE_0:def 4;
           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 A11: B = {x} \/ B by XBOOLE_1:12 .= {x} \/ X by XBOOLE_1:39;
         then card(X) + 1 = k + 1 by A9,A10,CARD_2:54,TARSKI:def 1;
         then A12: card(X) = k by XCMPLX_1:2;
           now assume X = {};
             hence contradiction by A7,A12,CARD_1:47,51;
             end;
         then reconsider X as non empty set;
         reconsider X as non empty finite set;
           now let u be set;
           assume u in X;
           then u in B by XBOOLE_0:def 4;
           hence u in Bags n;
           end;
         then reconsider X as non empty finite Subset of Bags n
           by TARSKI:def 3;
         consider b' being bag of n such that
         A13: b' in X &
             for b being bag of n st b in X holds [b,b'] in O by A8,A12;
         A14: O is_connected_in field O by RELAT_2:def 14;
           now per cases;
         case A15: x = b';
           take b';
           A16: X c= B by XBOOLE_1:36;
             now let b be bag of n;
             assume A17: b in B;
               now per cases;
             case b in X;
               hence [b,b'] in O by A13;
             case not(b in X);
               then b in {x} by A11,A17,XBOOLE_0:def 2;
               then b = x by TARSKI:def 1;
               hence [b,b'] in O by A15,ORDERS_1:12;
             end;
             hence [b,b'] in O;
             end;
           hence thesis by A13,A16;
         case A18: x <> b';
           A19: [x,x] in O by ORDERS_1:12;
             b' is Element of Bags n by POLYNOM1:def 14;
           then [b',b'] in O by ORDERS_1:12;
           then A20: x in field O & b' in field O by A19,RELAT_1:30;
             now per cases by A14,A18,A20,RELAT_2:def 6;
           case A21: [x,b'] in O;
             thus ex b' being bag of n st
                  b' in B &
                  for b being bag of n st b in B holds [b,b'] in O
             proof
             take b';
               for b being bag of n st b in B holds [b,b'] in O
               proof
               let b be bag of n;
               assume A22: b in B;
                 now per cases;
               case b <> x;
                 then not(b in {x}) by TARSKI:def 1;
                 then b in X by A22,XBOOLE_0:def 4;
                 hence thesis by A13;
               case b = x;
                 hence thesis by A21;
               end;
               hence thesis;
               end;
             hence thesis by A13,XBOOLE_0:def 4;
             end;
           case A23: [b',x] in O;
             thus ex b' being bag of n st
                  b' in B &
                  for b being bag of n st b in B holds [b,b'] 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 A24: b in B;
                 now per cases;
               case b <> x;
                 then not(b in {x}) by TARSKI:def 1;
                 then b in X by A24,XBOOLE_0:def 4;
                 then A25: [b,b'] in O by A13;
                   b is Element of Bags n & b' is Element of Bags n
                   by POLYNOM1:def 14;
                 hence thesis by A23,A25,ORDERS_1:14;
               case b = x;
                 hence thesis by ORDERS_1:12;
               end;
               hence thesis;
               end;
             hence thesis;
             end;
           end;
           hence thesis;
           end;
        hence thesis;
        end;
       thus thesis;
       end;
    end;
A26: for k being Nat st 1 <= k holds P[k] from Ind2(A2,A6);
reconsider sp = Support p as finite set by POLYNOM1:def 10;
  Card sp is finite;
then consider m being Nat such that
A27: Card(Support p) = Card m by CARD_1:86;
A28: Card(Support p) = m by A27,CARD_1:66;
  now assume m = 0;
  then card sp = 0 by A27,CARD_1:66;
  hence contradiction by A1,CARD_2:59;
  end;
then A29: 1 <= m by RLVECT_1:99;
reconsider sp = Support p as finite Subset of Bags n
  by POLYNOM1:def 10;
consider b' being bag of n such that
A30: b' in sp &
   for b being bag of n st b in sp holds [b,b'] in O by A26,A28,A29;
take b';
  now let b be bag of n;
  assume b in sp;
  then [b,b'] in O by A30;
  hence b <= b',O by Def2;
  end;
hence thesis by A30;
end;
uniqueness
proof
set O = T;
let b1,b2 be Element of Bags n;
assume A31: (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 A32: (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 A31,A32;
suppose Support p <> {};
  then b2 <= b1,O & b1 <= b2,O by A31,A32;
  then [b1,b2] in O & [b2,b1] in O by Def2;
  hence b1 = b2 by ORDERS_1:13;
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 :Def7:
  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 :Def8:
  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;
A1: now assume HC(p,O) = 0.L;
   then p.(HT(p,O)) = 0.L by Def7;
   then not(HT(p,O) in Support p) by POLYNOM1:def 9;
   then Support p = {} by Def6;
   hence p = 0_(n,L) by POLYNOM7:1;
   end;
  now assume p = 0_(n,L);
   then p.(HT(p,O)) = 0.L by POLYNOM1:81;
   hence HC(p,O) = 0.L by Def7;
   end;
hence thesis by A1;
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: HM(p,O) = Monom(HC(p,O),HT(p,O)) by Def8;
A2: p.(HT(p,O)) = HC(p,O) by Def7
              .= coefficient(HM(p,O)) by A1,POLYNOM7:9
              .= (HM(p,O)).term(HM(p,O)) by POLYNOM7:def 7;
  now per cases;
case HC(p,O) <> 0.L;
  then HC(p,O) is non-zero by RLVECT_1:def 13;
  hence term(HM(p,O)) = HT(p,O) by A1,POLYNOM7:10;
case A3: 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 A1,A3,POLYNOM7:8;
end;
hence thesis by A2;
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 p.(HT(p,O)) <> 0.L by Def7;
then (HM(p,O)).(HT(p,O)) <> 0.L by Lm8;
hence thesis by POLYNOM1:def 9;
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 A2: p = 0_(n,L) by Lm7;
then Support p = {} by POLYNOM7:1;
then A3: HT(p,O) = EmptyBag n by Def6;
then HM(p,O) = Monom(0.L,EmptyBag n) by A1,Def8;
then A4: term(HM(p,O)) = EmptyBag n by 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 A4,POLYNOM1:def 9;
  then p.(HT(p,O)) <> 0.L by A3,Lm8;
  hence contradiction by A2,POLYNOM1:81;
  end;
hence thesis;
end;

definition
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 2;
 case HC(p,O) = 0.L;
   then p = 0_(n,L) by Lm7;
   hence thesis by POLYNOM7:def 2;
 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 p.(HT(p,O)) = 0.L by Def7;
   then not(HT(p,O)) in Support p by POLYNOM1:def 9;
   then Support p = {} by Def6;
   then p = 0_(n,L) by POLYNOM7:1;
   hence contradiction by POLYNOM7:def 2;
 end;
 hence thesis by RLVECT_1:def 13;
 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 6
                  .= HT(m,O) by A1,Def6;
  hence HC(m,O) = m.(term(m)) by Def7 .= coefficient(m)
     by POLYNOM7:def 7;
  hence HM(m,O) = Monom(coefficient(m),term(m)) by A2,Def8
              .= m by POLYNOM7:11;
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 9;
    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 6;
  hence HC(m,O) = m.(term(m)) by Def7 .= coefficient(m)
    by POLYNOM7:def 7;
  hence HM(m,O) = Monom(coefficient(m),term(m)) by A6,Def8
              .= m by POLYNOM7:11;
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:81;
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: b1 is Element of Bags n & b is Element of Bags n
     by POLYNOM1:def 14;
    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 HM(p,O).b = 0.L by A2,A3,POLYNOM1:def 9;
  case HC(p,O) = 0.L;
    then Support(HM(p,O)) = {} by Lm10;
    then HM(p,O) = 0_(n,L) by POLYNOM7:1;
    hence HM(p,O).b = 0.L by POLYNOM1:81;
  end;
  hence thesis;
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 consider b being bag of n such that
A2: Support(HM(p,O)) = {b} by POLYNOM7:6;
  now per cases;
case HC(p,O) = 0.L;
  hence thesis by A1,Lm10;
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;
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;
  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 p = 0_(n,L) by Lm7;
      then p.(HT(p,O)) = 0.L by POLYNOM1:81;
      then (HM(p,O)).(HT(p,O)) = 0.L by Lm8;
      hence contradiction by A1,A2,POLYNOM1:def 9;
    case HC(p,O) <> 0.L;
      then p.(HT(p,O)) <> 0.L by Def7;
      hence u in Support p by A2,POLYNOM1:def 9;
    end;
    hence u in Support p;
  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;
A1: HM(p,O) = Monom(HC(p,O),HT(p,O)) by Def8;
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 A1,POLYNOM7:9;
suppose A2: not(HC(p,O) is non-zero);
    now per cases;
  case not(p is non-zero);
    then p = 0_(n,L) by POLYNOM7:def 2;
    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(Monom(HC(p,O),HT(p,O))) by A2,RLVECT_1:def 13
                .= term(HM(p,O)) by Def8;
    hence thesis by A1,POLYNOM7:9;
  case p is non-zero;
    then reconsider p as non-zero Polynomial of n,L;
      HC(p,O) is non-zero;
    hence thesis by A2;
  end;
  hence thesis;
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)
     = HT(Monom(HC(p,O),HT(p,O)),O) by Def8
    .= term(Monom(a,HT(p,O))) by Lm11
    .= HT(p,O) by POLYNOM7:10;
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 2;
    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(Monom(HC(p,O),HT(p,O))) by A1,RLVECT_1:def 13
                .= term(HM(p,O)) by Def8;
    hence thesis by Lm11;
  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;
  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 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(HM(p,O),O)) by Def7
                  .= (HM(p,O)).(HT(p,O)) by Th26
                  .= p.(HT(p,O)) by Lm8
                  .= HC(p,O) by Def7;
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_linear-order
holds R linearly_orders S
proof
  let X be set, S be Subset of X, R be Order of X;
  assume R is_linear-order;
then A1: R linearly_orders field R by ORDERS_2:35;
    S c= X;
  then S c= field R by ORDERS_2:2;
  hence thesis by A1,ORDERS_2:36;
end;

Lm14:
for n being Ordinal,
    O be admissible connected TermOrder of n,
    L being add-associative right_complementable left_zeroed right_zeroed
            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
         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 the carrier of L such that
A1: (p*'q).b = Sum s &
   len s = len decomp b &
   for k being 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 26;
consider S being non empty finite Subset of Bags n such that
A2: divisors b = SgmX(BagOrder n, S) &
   for p being bag of n holds p in S iff p divides b by POLYNOM1:def 18;
  HT(p,O) divides b by POLYNOM1:54;
then A3: HT(p,O) in S by A2;
set sgm = SgmX(BagOrder n, S);
  BagOrder n linearly_orders S by Lm13;
then HT(p,O) in rng(sgm) by A3,TRIANG_1:def 2;
then consider i being set such that
A4: i in dom sgm & sgm.i = HT(p,O) by FUNCT_1:def 5;
A5: i in dom decomp b by A2,A4,POLYNOM1:def 19;
  (divisors b)/.i = HT(p,O) by A2,A4,FINSEQ_4:def 4;
then A6: (decomp b)/.i = <*HT(p,O), b-'HT(p,O)*> by A5,POLYNOM1:def 19;
then A7: (decomp b)/.i = <*HT(p,O), HT(q,O)*> by POLYNOM1:52;
A8: dom s = Seg(len decomp b) by A1,FINSEQ_1:def 3
         .= dom(decomp b) by FINSEQ_1:def 3;
then A9: i in dom s by A2,A4,POLYNOM1:def 19;
reconsider i as Nat by A4;
A10:now let k be Nat;
  assume A11: k in dom s & k <> i;
  then consider b1', b2' being bag of n such that
  A12: (decomp b)/.k = <*b1', b2'*> & b = b1'+b2' by A8,POLYNOM1:72;
  consider b1,b2 being bag of n such that
  A13: (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by A1,A11;
  A14: b1 = <*b1', b2'*>.1 by A12,A13,FINSEQ_1:61
        .= b1' by FINSEQ_1:61;
  A15: b2 = <*b1', b2'*>.2 by A12,A13,FINSEQ_1:61
        .= b2' by FINSEQ_1:61;
  A16: now assume A17: p.b1 <> 0.L & q.b2 <> 0.L;
        b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14;
      then b1 in Support p & b2 in Support q by A17,POLYNOM1:def 9;
      then b1 <= HT(p,O),O & b2 <= HT(q,O),O by Def6;
      then A18: [b1,HT(p,O)] in O & [b2,HT(q,O)] in O by Def2;
      A19: now assume b1 = HT(p,O) & b2 = HT(q,O);
          then (decomp b).k
               = <*HT(p,O), HT(q,O)*> by A8,A11,A13,FINSEQ_4:def 4
              .= (decomp b)/.i by A6,POLYNOM1:52
              .= (decomp b).i by A5,FINSEQ_4:def 4;
          hence contradiction by A5,A8,A11,FUNCT_1:def 8;
          end;
        now per cases by A19;
      case A20: b1 <> HT(p,O);
        A21: now assume b1+b2 = HT(p,O)+b2;
            then b1 = (HT(p,O)+b2)-'b2 by POLYNOM1:52;
            hence contradiction by A20,POLYNOM1:52;
            end;
        A22: [HT(p,O)+HT(q,O), HT(p,O)+b2] in O by A12,A14,A15,A18,BAGORDER:def
7;
        A23: [HT(p,O)+b2, HT(p,O)+HT(q,O)] in O by A18,BAGORDER:def 7;
          HT(p,O)+b2 is Element of Bags n &
        HT(p,O)+HT(q,O) is Element of Bags n by POLYNOM1:def 14;
        hence contradiction by A12,A14,A15,A21,A22,A23,ORDERS_1:13;
      case A24: b2 <> HT(q,O);
        A25: now assume b2+b1 = HT(q,O)+b1;
            then b2 = (HT(q,O)+b1)-'b1 by POLYNOM1:52;
            hence contradiction by A24,POLYNOM1:52;
            end;
        A26: [HT(p,O)+HT(q,O), HT(q,O)+b1] in O by A12,A14,A15,A18,BAGORDER:def
7;
        A27: [HT(q,O)+b1, HT(p,O)+HT(q,O)] in O by A18,BAGORDER:def 7;
          HT(q,O)+b1 is Element of Bags n &
        HT(p,O)+HT(q,O) is Element of Bags n by POLYNOM1:def 14;
        hence contradiction by A12,A14,A15,A25,A26,A27,ORDERS_1:13;
      end;
      hence contradiction;
      end;
    now per cases by A16;
  case p.b1 = 0.L;
    hence p.b1*q.b2 = 0.L by BINOM:1;
  case q.b2 = 0.L;
    hence p.b1*q.b2 = 0.L by BINOM:2;
  end;
  hence s/.k = 0.L by A13;
  end;
consider b1,b2 being bag of n such that
A28: (decomp b)/.i = <*b1, b2*> & s/.i = p.b1*q.b2
   by A1,A9;
A29: b1 = <*HT(p,O), HT(q,O)*>.1 by A7,A28,FINSEQ_1:61
     .= HT(p,O) by FINSEQ_1:61;
  b2 = <*HT(p,O), HT(q,O)*>.2 by A7,A28,FINSEQ_1:61
  .= HT(q,O) by FINSEQ_1:61;
hence thesis by A1,A9,A10,A28,A29,POLYNOM2:5;
end;

theorem Th29:
for n being Ordinal,
    T being admissible connected TermOrder of n,
    L being add-associative right_complementable left_zeroed right_zeroed
            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
         unital distributive domRing-like (non trivial doubleLoopStr),
    p,q be non-zero Polynomial of n,L;
  p <> 0_(n,L) & q <> 0_(n,L) by POLYNOM7:def 2;
then Support p <> {} & Support q <> {} by POLYNOM7:1;
then HT(p,O) in Support p & HT(q,O) in Support q by Def6;
then A1: p.(HT(p,O)) <> 0.L & q.(HT(q,O)) <> 0.L by POLYNOM1:def 9;
set b = HT(p,O) + HT(q,O);
A2: b is Element of Bags n by POLYNOM1:def 14;
assume not(HT(p,O) + HT(q,O) in Support(p*'q));
then (p*'q).(HT(p,O) + HT(q,O)) = 0.L by A2,POLYNOM1:def 9;
then p.(HT(p,O)) * q.(HT(q,O)) = 0.L by Lm14;
hence thesis by A1,VECTSP_2:def 5;
end;

theorem Th30:
for n being Ordinal,
    L being add-associative right_complementable right_zeroed
            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
         unital distributive (non empty doubleLoopStr),
    p,q be Polynomial of n,L;
A1: now let b be bag of n;
    assume A2: b in Support(p*'q);
    then A3: (p*'q).b <> 0.L by POLYNOM1:def 9;
    consider s being FinSequence of the carrier of L such that A4:
    (p*'q).b = Sum s &
    len s = len decomp b &
    for k being 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 26;
    A5: dom s = Seg(len decomp b) by A4,FINSEQ_1:def 3
             .= dom(decomp b) by FINSEQ_1:def 3;
      now per cases;
    case dom s = {};
      then len s = 0 by FINSEQ_1:4,def 3;
      then s = <*>(the carrier of L) by FINSEQ_1:32;
      hence contradiction by A3,A4,RLVECT_1:60;
    case A6: dom s <> {};
      consider k being Element of dom s;
        k in dom s by A6;
      then reconsider k as Nat;
        now assume A7: 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);
          A8: for k being Nat st k in dom s holds s/.k = 0.L
              proof
              let k be Nat;
              assume A9: k in dom s;
              then consider b1, b2 being bag of n such that
              A10: (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by A4;
                now per cases by A5,A7,A9,A10;
              case p.b1 = 0.L;
                hence 0.L = s/.k by A10,BINOM:1;
              case q.b2 = 0.L;
                hence 0.L = s/.k by A10,BINOM:2;
              end;
              hence thesis;
              end;
          then for k' being Nat st k' in dom s & k' <> k holds s/.k' = 0.L;
          then Sum s = s/.k by A6,POLYNOM2:5
                    .= 0.L by A6,A8;
          hence contradiction by A2,A4,POLYNOM1:def 9;
          end;
      then consider k being Element of dom(decomp b),
                      b1,b2 being bag of n such that
      A11: (decomp b)/.k = <*b1, b2*> & p.b1 <> 0.L & q.b2 <> 0.L;
        k in dom(decomp b) by A5,A6;
      then reconsider k as Nat;
        b1 is Element of Bags n & b2 is Element of Bags n by POLYNOM1:def 14;
      then A12: b1 in Support p & b2 in Support q by A11,POLYNOM1:def 9;
      consider b1', b2' being bag of n such that
      A13: (decomp b)/.k = <*b1', b2'*> & b = b1'+b2' by A5,A6,POLYNOM1:72;
      A14: b1' = <*b1, b2*>.1 by A11,A13,FINSEQ_1:61
              .= b1 by FINSEQ_1:61;
        b2' = <*b1, b2*>.2 by A11,A13,FINSEQ_1:61
         .= b2 by FINSEQ_1:61;
      hence ex s,t being bag of n
        st s in Support p & t in Support q & b = s+t by A12,A13,A14;
      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 A15: u in Support(p*'q);
  then reconsider u' = u as Element of Bags n;
  consider s,t being bag of n such that
  A16: s in Support p & t in Support q & u' = s+t by A1,A15;
  thus u in {s' + t' where s',t' is Element of Bags n :
                        s' in Support p & t' in Support q} by A16;
  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
            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
         unital distributive domRing-like (non trivial doubleLoopStr),
    p,q be non-zero Polynomial of n,L;
  Support p*'q <> {} by Th29;
then A1: HT(p*'q,O) in Support(p*'q) by Def6;
  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) 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 A1;
then consider s,t being Element of Bags n such that
A3: HT(p*'q,O) = s + t & s in Support p & t in Support q;
  s <= HT(p,O),O & t <= HT(q,O),O by A3,Def6;
then A4: [s,HT(p,O)] in O & [t,HT(q,O)] in O by Def2;
A5: s + t is Element of Bags n &
    HT(p,O) + t is Element of Bags n &
    HT(p*'q,O) is Element of Bags n &
    HT(p,O)+HT(q,O) is Element of Bags n by POLYNOM1:def 14;
A6: [s + t,HT(p,O) + t] in O by A4,BAGORDER:def 7;
  [t + HT(p,O), HT(p,O)+HT(q,O)] in O by A4,BAGORDER:def 7;
then [s + t,HT(p,O)+HT(q,O)] in O by A5,A6,ORDERS_1:14;
hence thesis by A2,A3,A5,ORDERS_1:13;
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
            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
         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*'q,O)) by Def7
          .= (p*'q).(HT(p,O) + HT(q,O)) by Th31
          .= p.(HT(p,O)) * q.(HT(q,O)) by Lm14
          .= HC(p,O) * q.(HT(q,O)) by Def7
          .= HC(p,O) * HC(q,O) by Def7;
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
            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
         unital distributive domRing-like (non trivial doubleLoopStr),
    p,q be non-zero Polynomial of n,L;
  thus HM(p*'q,O) = Monom(HC(p*'q,O),HT(p*'q,O)) by Def8
                 .= 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
                 .= Monom(HC(p,O),HT(p,O)) *' Monom(HC(q,O),HT(q,O)) by Th3
                 .= HM(p,O) *' Monom(HC(q,O),HT(q,O)) by Def8
                 .= HM(p,O) *' HM(q,O) by Def8;
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 LoopStr),
    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 LoopStr),
    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:79;
    now per cases by A1,A2,XBOOLE_0:def 2;
  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;
    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;
    hence thesis;
  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;
    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;
    hence thesis;
  end;
  hence thesis;
suppose not(HT(p+q,O) in Support(p+q));
  then Support(p+q) = {} & 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 7;
  hence thesis by Def2;
end;

begin :: Reductum

definition
::: definition 5.15, p. 194
let n be Ordinal,
    T be connected TermOrder of n,
    L be add-associative right_complementable right_zeroed
         (non empty LoopStr),
    p be Polynomial of n,L;
func Red(p,T) -> Polynomial of n,L equals :Def9:
  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 LoopStr),
    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 LoopStr),
    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 9;
then (p - HM(p,O)).(HT(p,O)) <> 0.L by Def9;
then (p + -HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 23;
then p.(HT(p,O)) + (-HM(p,O)).(HT(p,O)) <> 0.L by POLYNOM1:def 21;
then A1: p.(HT(p,O)) + -HM(p,O).(HT(p,O)) <> 0.L by POLYNOM1:def 22;
  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 LoopStr),
    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 LoopStr),
    p being Polynomial of n,L,
    b being bag of n;
assume A1: b in Support p & b <> HT(p,O);
A2: b is Element of Bags n by POLYNOM1:def 14;
  (Red(p,O)).b = (p - HM(p,O)).b by Def9
            .= (p + -HM(p,O)).b by POLYNOM1:def 23
            .= p.b + (-HM(p,O)).b by POLYNOM1:def 21
            .= p.b + -HM(p,O).b by POLYNOM1:def 22
            .= p.b + - 0.L by A1,Th19
            .= p.b + 0.L by RLVECT_1:25
            .= p.b by RLVECT_1:10;
then (Red(p,O)).b <> 0.L by A1,POLYNOM1:def 9;
hence thesis by A2,POLYNOM1:def 9;
end;

Lm17:
for n being Ordinal,
    O being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    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 LoopStr),
    p being Polynomial of n,L;
A1: now let u be set;
   assume u in Support(p) \ {HT(p,O)};
   then A2: u in Support p & not(u in {HT(p,O)}) by XBOOLE_0:def 4;
   then reconsider u' = u as Element of Bags n;
   reconsider u' as bag of n;
     u' <> HT(p,O) by A2,TARSKI:def 1;
   hence u in Support(Red(p,O)) by A2,Lm16;
   end;
  now let u be set;
   assume A3: u in Support(Red(p,O));
   then A4: u in Support(p - HM(p,O)) by Def9;
   reconsider u' = u as Element of Bags n by A3;
   reconsider u' as bag of n;
   A5: (p - HM(p,O)).u' <> 0.L by A4,POLYNOM1:def 9;
   A6: (p + -HM(p,O)).u' = p.u' + (-HM(p,O)).u' by POLYNOM1:def 21
                       .= p.u' + -HM(p,O).u' by POLYNOM1:def 22;
   A7: not(u' = HT(p,O)) by A3,Lm15;
   then (p + -HM(p,O)).u' = p.u' + - 0.L by A6,Th19
                         .= p.u' + 0.L by RLVECT_1:25
                         .= p.u' by RLVECT_1:10;
   then p.u' <> 0.L by A5,POLYNOM1:def 23;
   then A8: u' in Support p by POLYNOM1:def 9;
     not(u' in {HT(p,O)}) by A7,TARSKI:def 1;
   hence u in Support(p) \ {HT(p,O)} by A8,XBOOLE_0:def 4;
   end;
hence thesis by A1,TARSKI:2;
end;

theorem
  for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    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 LoopStr),
    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 LoopStr),
    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 LoopStr),
    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 LoopStr),
    p be Polynomial of n,L;
A1: HT(p,O) in {HT(p,O)} by TARSKI:def 1;
  Support(Red(p,O)) = Support(p) \ {HT(p,O)} by Lm17;
then not(HT(p,O) in Support(Red(p,O))) by A1,XBOOLE_0:def 4;
hence thesis by POLYNOM1:def 9;
end;

Lm19:
for n being Ordinal,
    O being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    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 LoopStr),
    p be Polynomial of n,L,
    b be bag of n;
assume b <> HT(p,O);
then not(b in {HT(p,O)}) by TARSKI:def 1;
then A1: not(b in Support(HM(p,O))) by Lm12;
A2: b is Element of Bags n by POLYNOM1:def 14;
thus (Red(p,O)).b = (p - HM(p,O)).b by Def9
          .= (p + -HM(p,O)).b by POLYNOM1:def 23
          .= p.b + (-HM(p,O)).b by POLYNOM1:def 21
          .= p.b + -(HM(p,O)).b by POLYNOM1:def 22
          .= p.b + -0.L by A1,A2,POLYNOM1:def 9
          .= p.b + 0.L by RLVECT_1:25
          .= p.b by RLVECT_1:10;
end;

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

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

theorem
  for n being Ordinal,
    T being connected TermOrder of n,
    L being add-associative right_complementable right_zeroed
            (non trivial LoopStr),
    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 LoopStr),
    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;

Back to top