termord.miz



    begin

    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;

      :: TERMORD:def1

      attr b is zero means b = ( EmptyBag X);

    end

    theorem :: TERMORD:1

    

     Th1: for X be set, b1,b2 be bag of X holds b1 divides b2 iff ex b be 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 object;

          (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 be bag of n st b2 = (b1 + b);

          end;

            case n <> {} ;

            then

            reconsider n9 = n as non empty set;

            set b = the set of all [k, ((b2 . k) -' (b1 . k))] where k be Element of n9;

             A4:

            now

              let x be object;

              assume x in b;

              then ex k be Element of n9 st x = [k, ((b2 . k) -' (b1 . k))];

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

            end;

            now

              let x,y1,y2 be object;

              assume that

               A5: [x, y1] in b and

               A6: [x, y2] in b;

              consider k be Element of n9 such that

               A7: [x, y1] = [k, ((b2 . k) -' (b1 . k))] by A5;

              consider k9 be 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 object;

              assume x in ( dom b);

              then

              consider y be object such that

               A10: [x, y] in b by XTUPLE_0:def 12;

              consider k be 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 object;

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

            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 be object such that

               A14: [k, u] in b by A12, XTUPLE_0:def 12;

              consider k9 be 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 object;

              

               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);

            now

              let x be object;

              assume x in ( rng b);

              then

              consider y be object such that

               A21: [y, x] in b by XTUPLE_0:def 13;

              consider k be 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 ;

            then

            reconsider b as bag of n by A20, PRE_POLY:def 8, VALUED_0:def 6;

            take b;

            now

              let k be object;

              

               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 be bag of n st b2 = (b1 + b);

          end;

        end;

        hence ex b be bag of n st b2 = (b1 + b);

      end;

      hence thesis by PRE_POLY: 50;

    end;

    theorem :: TERMORD:2

    

     Th2: for n be Ordinal, L be add-associative right_complementable right_zeroed well-unital distributive non empty doubleLoopStr, p be Series of n, L holds (( 0_ (n,L)) *' p) = ( 0_ (n,L))

    proof

      let n be Ordinal, L be add-associative right_complementable right_zeroed 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 be FinSequence of L such that

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

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

        now

          let k be Nat;

          assume k in ( dom s);

          then

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

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

          

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

          .= ( 0. L);

        end;

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    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 be 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 4;

               A5:

              now

                let b be bag of n;

                assume

                 A6: b <> mb2;

                consider b9 be bag of n such that

                 A7: for b be 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 be 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 4;

               A10:

              now

                let b be bag of n;

                assume

                 A11: b <> mb1;

                consider b9 be bag of n such that

                 A12: for b be 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 be FinSequence of L such that

               A14: ((m1 *' m2) . b) = ( Sum s) and

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

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

              

               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 be bag of n such that

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

                   A23: (s /. k) = ((m1 . b1) * (m2 . b2)) by A16;

                  consider b19,b29 be 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);

                    end;

                      case b2 <> mb2;

                      then (m2 . b2) = ( 0. L) by A5;

                      hence ((m1 . b1) * (m2 . b2)) = ( 0. L);

                    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 be 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 4;

              end;

              now

                let b9 be bag of n;

                assume

                 A30: b9 <> b;

                consider s be FinSequence of L such that

                 A31: ((m1 *' m2) . b9) = ( Sum s) and

                 A32: ( len s) = ( len ( decomp b9)) and

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

                

                 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 be bag of n such that

                   A37: (( decomp b9) /. k) = <*b1, b2*> and

                   A38: (s /. k) = ((m1 . b1) * (m2 . b2)) by A33;

                  consider b19,b29 be 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);

                    end;

                      case b2 <> mb2;

                      then (m2 . b2) = ( 0. L) by A5;

                      hence ((m1 . b1) * (m2 . b2)) = ( 0. L);

                    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 be 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 be FinSequence of L such that

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

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

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

          

           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 be bag of n such that

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

             A9: (s /. k) = ((c1 . b1) * (c2 . b2)) by A4;

            consider b19,b29 be 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;

              end;

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

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

              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 be 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 :: TERMORD:3

    

     Th3: for 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 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 be FinSequence of L such that

       A1: (m3 . (b + b9)) = ( Sum s) and

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

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

      set u = (b + b9);

      consider k9 be 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 be 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 be bag of n such that

         A15: for b9 be 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 be bag of n such that

         A21: for b9 be 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 be 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);

          end;

            case b2 <> b9;

            then (m2 . b2) = ( 0. L) by A12;

            hence ((m1 . b1) * (m2 . b2)) = ( 0. L);

          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 :: TERMORD:4

    for 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 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);

            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);

            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

    

     Lm1: for n be Ordinal, T be TermOrder of n, b be 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 object;

          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

    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;

      :: TERMORD:def2

      pred b <= b9,T means [b, b9] in T;

    end

    definition

      let n be Ordinal, T be TermOrder of n, b,b9 be bag of n;

      :: TERMORD:def3

      pred b < b9,T means b <= (b9,T) & b <> b9;

    end

    definition

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

      :: TERMORD:def4

      func min (b1,b2,T) -> bag of n equals

      : Def4: b1 if b1 <= (b2,T)

      otherwise b2;

      correctness ;

      :: TERMORD:def5

      func max (b1,b2,T) -> bag of n equals

      : Def5: b1 if b2 <= (b1,T)

      otherwise b2;

      correctness ;

    end

    

     Lm2: for n be Ordinal, T be TermOrder of n, b be 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;

    end;

    

     Lm3: for n be Ordinal, T be TermOrder of n, b1,b2 be 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;

      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 be Ordinal, T be TermOrder of n, b be 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 :: TERMORD:5

    

     Th5: for n be Ordinal, T be connected TermOrder of n, b1,b2 be 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 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;

              case

               A5: not b2 <= (b1,T);

              

               A6: b1 in ( field T) & b2 in ( field T) by Lm4;

               not [b2, b1] in T by A5;

              then [b1, b2] in T by A1, A2, A6, RELAT_2:def 6;

              hence thesis;

            end;

              case b1 = b2;

              hence thesis by A2;

            end;

          end;

          hence thesis;

        end;

        b1 <= (b2,T) implies not b2 < (b1,T) by Lm3;

        hence thesis by A3;

      end;

    end;

    

     Lm5: for n be Ordinal, T be connected TermOrder of n, b1,b2 be 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;

      end;

        suppose

         A4: b1 <> b2;

        assume not b1 <= (b2,T);

        then

         A5: not [b1, b2] in T;

        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;

      end;

    end;

    theorem :: TERMORD:6

    for n be Ordinal, T be TermOrder of n, b be bag of n holds b <= (b,T) by Lm2;

    theorem :: TERMORD:7

    for n be Ordinal, T be TermOrder of n, b1,b2 be bag of n st b1 <= (b2,T) & b2 <= (b1,T) holds b1 = b2 by Lm3;

    theorem :: TERMORD:8

    

     Th8: for n be Ordinal, T be TermOrder of n, b1,b2,b3 be 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;

      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;

    end;

    theorem :: TERMORD:9

    

     Th9: for n be Ordinal, T be admissible TermOrder of n, b be bag of n holds ( EmptyBag n) <= (b,T) by BAGORDER:def 5;

    theorem :: TERMORD:10

    for n be Ordinal, T be admissible TermOrder of n, b1,b2 be 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 be bag of n such that

       A1: b2 = (b1 + b3) by Th1;

      ( EmptyBag n) <= (b3,T) by Th9;

      then [( EmptyBag n), b3] in T;

      then [(( EmptyBag n) + b1), b2] in T by A1, BAGORDER:def 5;

      then [b1, b2] in T by PRE_POLY: 53;

      hence thesis;

    end;

    theorem :: TERMORD:11

    

     Th11: for n be Ordinal, T be TermOrder of n, b1,b2 be 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 :: TERMORD:12

    

     Th12: for n be Ordinal, T be TermOrder of n, b1,b2 be 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 be Ordinal, T be TermOrder of n, b be bag of n holds ( min (b,b,T)) = b & ( max (b,b,T)) = b by Def4, Def5;

    theorem :: TERMORD:13

    for n be Ordinal, T be connected TermOrder of n, b1,b2 be 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;

            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 :: TERMORD:14

    

     Th14: for n be Ordinal, T be connected TermOrder of n, b1,b2 be 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;

            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 :: TERMORD:15

    

     Th15: for n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n holds ( min (b1,b2,T)) = ( min (b2,b1,T)) & ( max (b1,b2,T)) = ( max (b2,b1,T))

    proof

      let n be Ordinal, T be connected TermOrder of n, b1,b2 be 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 :: TERMORD:16

    for n be Ordinal, T be connected TermOrder of n, b1,b2 be bag of n holds ( min (b1,b2,T)) = b1 iff ( max (b1,b2,T)) = b2

    proof

      let n be Ordinal, T be connected TermOrder of n, b1,b2 be 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

    definition

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

      :: TERMORD:def6

      func HT (p,T) -> Element of ( Bags n) means

      : Def6: ( Support p) = {} & it = ( EmptyBag n) or (it in ( Support p) & for b be 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 5;

          ( card sp) is finite;

          then

          consider m be 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 5;

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

          

           A3: for k be 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 object;

                  assume u in {x};

                  then u = x by TARSKI:def 1;

                  hence u in B;

                end;

                then {x} c= B;

                

                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 be bag of n such that

                 A9: b9 in X and

                 A10: for b be 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 be bag of n st b9 in B & for b be bag of n st b in B holds [b, b9] in O

                        proof

                          take b9;

                          for b be 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 be bag of n st b9 in B & for b be bag of n st b in B holds [b, b9] in O

                        proof

                          take x;

                          for b be 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;

          

           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 be object 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 be Nat st 1 <= k holds P[k] from NAT_1:sch 8( A25, A3);

          then

          consider b9 be bag of n such that

           A28: b9 in sp and

           A29: for b be bag of n st b in sp holds [b, b9] in O by A24, A23;

          take b9;

          for b be bag of n st b in sp holds b <= (b9,O) by A29;

          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 be 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 be 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;

          b2 <= (b1,O) by A30, A31, A32;

          then [b2, b1] in O;

          hence b1 = b2 by A33, ORDERS_1: 4;

        end;

      end;

    end

    definition

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

      :: TERMORD:def7

      func HC (p,T) -> Element of L equals (p . ( HT (p,T)));

      correctness ;

    end

    definition

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

      :: TERMORD:def8

      func HM (p,T) -> Monomial of n, L equals ( Monom (( HC (p,T)),( HT (p,T))));

      correctness ;

    end

    

     Lm7: for n be 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 4;

        then ( Support p) = {} by Def6;

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

      end;

      hence thesis by POLYNOM1: 22;

    end;

    

     Lm8: for n be 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 be 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 be 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 be 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 4;

    end;

    

     Lm10: for n be 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 be 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 4;

        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 4;

          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 be Ordinal, O be connected TermOrder of n, L be non empty ZeroStr, m be 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 be bag of n st ( Support m) = {b};

        then

        consider b be 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 4;

        ( 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 :: TERMORD:17

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

    theorem :: TERMORD:18

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

    theorem :: TERMORD:19

    

     Th19: for n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n, L, b be bag of n st b <> ( HT (p,T)) holds (( HM (p,T)) . b) = ( 0. L)

    proof

      let n be Ordinal, O be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n, L, b be 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 be bag of n st ( Support ( HM (p,O))) = {b};

        then

        consider b1 be 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 4;

          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 be 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 be 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 :: TERMORD:20

    for n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be 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;

      let u be object;

      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 4;

            end;

              case ( HC (p,O)) <> ( 0. L);

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

            end;

          end;

          hence u in ( Support p);

        end;

      end;

      hence u in ( Support p);

    end;

    theorem :: TERMORD:21

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

    theorem :: TERMORD:22

    for n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be 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 :: TERMORD:23

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

    theorem :: TERMORD:24

    for n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, c be 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 :: TERMORD:25

    for n be Ordinal, T be connected TermOrder of n, L be non empty ZeroStr, a be 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 :: TERMORD:26

    

     Th26: for n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be 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 :: TERMORD:27

    for n be Ordinal, T be connected TermOrder of n, L be non trivial ZeroStr, p be Polynomial of n, L holds ( HC (( HM (p,T)),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;

      

      thus ( HC (( HM (p,O)),O)) = (( HM (p,O)) . ( HT (p,O))) by Th26

      .= ( HC (p,O)) by Lm8;

    end;

    theorem :: TERMORD:28

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

    

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

    proof

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

      S c= X;

      then

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

      assume R is being_linear-order;

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

    end;

    

     Lm14: for n be Ordinal, O be admissible connected TermOrder of n, L be add-associative right_complementable left_zeroed right_zeroed well-unital distributive non trivial doubleLoopStr, p,q be 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 be FinSequence of L such that

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

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

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

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

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

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

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

      

       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 be object 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 be 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 be 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 be 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 4;

          then b1 <= (( HT (p,O)),O) by Def6;

          then

           A29: [b1, ( HT (p,O))] in O;

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

          then b2 in ( Support q) by A28, POLYNOM1:def 4;

          then b2 <= (( HT (q,O)),O) by Def6;

          then

           A30: [b2, ( HT (q,O))] in O;

           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);

          end;

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

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

          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 :: TERMORD:29

    

     Th29: for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable left_zeroed right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p,q be 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 4;

      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 4;

      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 4;

      then ((p . ( HT (p,O))) * (q . ( HT (q,O)))) = ( 0. L) by Lm14;

      hence thesis by A2, A3, VECTSP_2:def 1;

    end;

    theorem :: TERMORD:30

    

     Th30: for n be Ordinal, L be add-associative right_complementable right_zeroed well-unital distributive non empty doubleLoopStr, p,q be Polynomial of n, L holds ( Support (p *' q)) c= { (s + t) where s,t be 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 be FinSequence of L such that

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

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

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

        

         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 be Element of ( dom ( decomp b)), b1,b2 be bag of n st (( decomp b) /. k) = <*b1, b2*> & (p . b1) <> ( 0. L) & (q . b2) <> ( 0. L));

              

               A9: for k be 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 be 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;

                  end;

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

                    hence thesis by A12;

                  end;

                end;

                hence thesis;

              end;

              then for k9 be 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 4;

            end;

            then

            consider k be Element of ( dom ( decomp b)), b1,b2 be 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 be 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 4;

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

            then

             A20: b1 in ( Support p) by A14, POLYNOM1:def 4;

            b19 = ( <*b1, b2*> . 1) by A13, A16, FINSEQ_1: 44

            .= b1 by FINSEQ_1: 44;

            hence ex s,t be 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 be bag of n st s in ( Support p) & t in ( Support q) & b = (s + t);

      end;

      now

        let u be object;

        assume

         A21: u in ( Support (p *' q));

        then

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

        ex s,t be 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 be Element of ( Bags n) : s9 in ( Support p) & t9 in ( Support q) };

      end;

      hence thesis;

    end;

    theorem :: TERMORD:31

    

     Th31: for n be Ordinal, T 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 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;

      ( 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 be 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 be Element of ( Bags n) : s in ( Support p) & t in ( Support q) } by A3;

      then

      consider s,t be 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;

      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;

      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 :: TERMORD:32

    

     Th32: for n be Ordinal, T 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 holds ( HC ((p *' q),T)) = (( HC (p,T)) * ( HC (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;

      

      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 :: TERMORD:33

    for n be Ordinal, T 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 holds ( HM ((p *' q),T)) = (( HM (p,T)) *' ( HM (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;

      

      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 :: TERMORD:34

    for n be Ordinal, T be admissible connected TermOrder of n, L be right_zeroed non empty addLoopStr, p,q be Polynomial of n, L holds ( HT ((p + q),T)) <= (( max (( HT (p,T)),( HT (q,T)),T)),T)

    proof

      let n be Ordinal, O be 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;

      end;

    end;

    begin

    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;

      :: TERMORD:def9

      func Red (p,T) -> Polynomial of n, L equals (p - ( HM (p,T)));

      coherence ;

    end

    

     Lm15: for n be Ordinal, O be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds not (( HT (p,O)) in ( Support ( Red (p,O))))

    proof

      let n be Ordinal, O be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be 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 4;

      then ((p + ( - ( HM (p,O)))) . ( HT (p,O))) <> ( 0. L) by POLYNOM1:def 7;

      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 be Ordinal, O be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L, b be bag of n st b in ( Support p) & b <> ( HT (p,O)) holds b in ( Support ( Red (p,O)))

    proof

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

      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 7

      .= ((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 4;

      hence thesis by POLYNOM1:def 4;

    end;

    

     Lm17: for n be Ordinal, O be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds ( Support ( Red (p,O))) = (( Support p) \ {( HT (p,O))})

    proof

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

       A1:

      now

        let u be object;

        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 4;

        

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

        then

         A5: u9 in ( Support p) by POLYNOM1:def 4;

         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 object;

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

    end;

    theorem :: TERMORD:35

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds ( Support ( Red (p,T))) c= ( Support p)

    proof

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

      ( Support ( Red (p,O))) = (( Support p) \ {( HT (p,O))}) by Lm17;

      hence thesis by XBOOLE_1: 36;

    end;

    theorem :: TERMORD:36

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds ( Support ( Red (p,T))) = (( Support p) \ {( HT (p,T))}) by Lm17;

    

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

    proof

      let n be Ordinal, O be 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 4;

    end;

    

     Lm19: for n be Ordinal, O be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L, b be bag of n st b <> ( HT (p,O)) holds (( Red (p,O)) . b) = (p . b)

    proof

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

      

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

      assume 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 7

      .= ((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 4

      .= ((p . b) + ( 0. L)) by RLVECT_1: 12

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

    end;

    theorem :: TERMORD:37

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds ( Support (( HM (p,T)) + ( Red (p,T)))) = ( Support p)

    proof

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

       A1:

      now

        let u be object;

        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 4;

        now

          per cases ;

            case

             A4: u9 = ( HT (p,O));

            then

             A5: (p . ( HT (p,O))) <> ( 0. L) by A2, POLYNOM1:def 4;

            ((( 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 4;

          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 4;

          end;

        end;

        hence u in ( Support (( HM (p,O)) + ( Red (p,O))));

      end;

      now

        let u be object;

        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 4;

        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 4;

          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 4;

          end;

        end;

        hence u in ( Support p);

      end;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: TERMORD:38

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds (( HM (p,T)) + ( Red (p,T))) = p

    proof

      let n be Ordinal, O be 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 object;

        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 :: TERMORD:39

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L holds (( Red (p,T)) . ( HT (p,T))) = ( 0. L) by Lm18;

    theorem :: TERMORD:40

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr, p be Polynomial of n, L, b be bag of n st b in ( Support p) & b <> ( HT (p,T)) holds (( Red (p,T)) . b) = (p . b) by Lm19;