groeb_3.miz



    begin

    theorem :: GROEB_3:1

    

     Th1: for X be set, b1,b2 be bag of X holds ((b1 + b2) / b2) = b1

    proof

      let X be set, b1,b2 be bag of X;

      b2 divides (b1 + b2) by PRE_POLY: 50;

      then (b2 + ((b1 + b2) / b2)) = (b1 + b2) by GROEB_2:def 1;

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

      hence thesis by PRE_POLY: 48;

    end;

    theorem :: GROEB_3:2

    

     Th2: for n be Ordinal, T be admissible TermOrder of n, b1,b2,b3 be bag of n holds b1 <= (b2,T) implies (b1 + b3) <= ((b2 + b3),T)

    proof

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

      assume b1 <= (b2,T);

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

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

      hence thesis by TERMORD:def 2;

    end;

    theorem :: GROEB_3:3

    

     Th3: for n be Ordinal, T be TermOrder of n, b1,b2,b3 be bag of n holds b1 <= (b2,T) & b2 < (b3,T) implies b1 < (b3,T)

    proof

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

      assume that

       A1: b1 <= (b2,T) and

       A2: b2 < (b3,T);

      

       A3: b2 <= (b3,T) by A2, TERMORD:def 3;

      then

       A4: b1 <= (b3,T) by A1, TERMORD: 8;

      b2 <> b3 by A2, TERMORD:def 3;

      then b1 <> b3 by A1, A3, TERMORD: 7;

      hence thesis by A4, TERMORD:def 3;

    end;

    theorem :: GROEB_3:4

    

     Th4: for n be Ordinal, T be admissible TermOrder of n, b1,b2,b3 be bag of n holds b1 < (b2,T) implies (b1 + b3) < ((b2 + b3),T)

    proof

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

      assume

       A1: b1 < (b2,T);

       A2:

      now

        assume

         A3: (b1 + b3) = (b2 + b3);

        b1 = ((b1 + b3) -' b3) by PRE_POLY: 48

        .= b2 by A3, PRE_POLY: 48;

        hence contradiction by A1, TERMORD:def 3;

      end;

      b1 <= (b2,T) by A1, TERMORD:def 3;

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

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

      then (b1 + b3) <= ((b2 + b3),T) by TERMORD:def 2;

      hence thesis by A2, TERMORD:def 3;

    end;

    theorem :: GROEB_3:5

    

     Th5: for n be Ordinal, T be admissible TermOrder of n, b1,b2,b3,b4 be bag of n holds b1 < (b2,T) & b3 <= (b4,T) implies (b1 + b3) < ((b2 + b4),T)

    proof

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

      assume that

       A1: b1 < (b2,T) and

       A2: b3 <= (b4,T);

      b1 <= (b2,T) by A1, TERMORD:def 3;

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

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

      then

       A3: (b1 + b3) <= ((b2 + b3),T) by TERMORD:def 2;

       [b3, b4] in T by A2, TERMORD:def 2;

      then [(b2 + b3), (b2 + b4)] in T by BAGORDER:def 5;

      then

       A4: (b2 + b3) <= ((b2 + b4),T) by TERMORD:def 2;

       A5:

      now

        

         A6: b1 = ((b1 + b4) -' b4) & b2 = ((b2 + b4) -' b4) by PRE_POLY: 48;

        

         A7: b4 = ((b4 + b2) -' b2) & b3 = ((b3 + b2) -' b2) by PRE_POLY: 48;

        assume (b1 + b3) = (b2 + b4);

        then (b1 + b4) = (b2 + b4) by A3, A4, A7, TERMORD: 7;

        hence contradiction by A1, A6, TERMORD:def 3;

      end;

      (b1 + b3) <= ((b2 + b4),T) by A3, A4, TERMORD: 8;

      hence thesis by A5, TERMORD:def 3;

    end;

    theorem :: GROEB_3:6

    

     Th6: for n be Ordinal, T be admissible TermOrder of n, b1,b2,b3,b4 be bag of n holds b1 <= (b2,T) & b3 < (b4,T) implies (b1 + b3) < ((b2 + b4),T)

    proof

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

      assume that

       A1: b1 <= (b2,T) and

       A2: b3 < (b4,T);

      b3 <= (b4,T) by A2, TERMORD:def 3;

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

      then [(b2 + b3), (b2 + b4)] in T by BAGORDER:def 5;

      then

       A3: (b2 + b3) <= ((b2 + b4),T) by TERMORD:def 2;

       [b1, b2] in T by A1, TERMORD:def 2;

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

      then

       A4: (b1 + b3) <= ((b2 + b3),T) by TERMORD:def 2;

       A5:

      now

        assume (b1 + b3) = (b2 + b4);

        then

         A6: (b2 + b4) = (b2 + b3) by A4, A3, TERMORD: 7;

        b4 = ((b4 + b2) -' b2) & b3 = ((b3 + b2) -' b2) by PRE_POLY: 48;

        hence contradiction by A2, A6, TERMORD:def 3;

      end;

      (b1 + b3) <= ((b2 + b4),T) by A4, A3, TERMORD: 8;

      hence thesis by A5, TERMORD:def 3;

    end;

    begin

    theorem :: GROEB_3:7

    

     Th7: for n be Ordinal, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, m1,m2 be non-zero Monomial of n, L holds ( term (m1 *' m2)) = (( term m1) + ( term m2))

    proof

      let n be Ordinal, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, m1,m2 be non-zero Monomial of n, L;

      set T = the connected TermOrder of n;

      

       A1: ( HC (m2,T)) <> ( 0. L);

      ( HC (m1,T)) <> ( 0. L);

      then

      reconsider a = ( coefficient m1), b = ( coefficient m2) as non zero Element of L by A1, TERMORD: 23;

      (a * b) <> ( 0. L) by VECTSP_2:def 1;

      then

      reconsider c = (a * b) as non zero Element of L by STRUCT_0:def 12;

      m1 = ( Monom (a,( term m1))) & m2 = ( Monom (b,( term m2))) by POLYNOM7: 11;

      then ( term (m1 *' m2)) = ( term ( Monom (c,(( term m1) + ( term m2))))) by TERMORD: 3;

      hence thesis by POLYNOM7: 10;

    end;

    theorem :: GROEB_3:8

    

     Th8: for n be Ordinal, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, m be non-zero Monomial of n, L, b be bag of n holds b in ( Support p) iff (( term m) + b) in ( Support (m *' p))

    proof

      let n be Ordinal, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, m be non-zero Monomial of n, L, b be bag of n;

      

       A1: ((m *' p) . (( term m) + b)) = ((m . ( term m)) * (p . b)) by POLYRED: 7;

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

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

      then ( Support m) = {( term m)} by POLYNOM7: 7;

      then ( term m) in ( Support m) by TARSKI:def 1;

      then

       A2: (m . ( term m)) <> ( 0. L) by POLYNOM1:def 4;

       A3:

      now

        assume b in ( Support p);

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

        then (( term m) + b) is Element of ( Bags n) & ((m *' p) . (( term m) + b)) <> ( 0. L) by A2, A1, PRE_POLY:def 12, VECTSP_2:def 1;

        hence (( term m) + b) in ( Support (m *' p)) by POLYNOM1:def 4;

      end;

      now

        assume (( term m) + b) in ( Support (m *' p));

        then ((m . ( term m)) * (p . b)) <> ( 0. L) by A1, POLYNOM1:def 4;

        then

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

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

        hence b in ( Support p) by A4, POLYNOM1:def 4;

      end;

      hence thesis by A3;

    end;

    theorem :: GROEB_3:9

    

     Th9: for n be Ordinal, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, m be non-zero Monomial of n, L holds ( Support (m *' p)) = { (( term m) + b) where b be Element of ( Bags n) : b in ( Support p) }

    proof

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

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

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

      then

       A1: ( Support m) = {( term m)} by POLYNOM7: 7;

      

       A2: ( Support (m *' p)) c= { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support p) } by TERMORD: 30;

       A3:

      now

        let u be object;

        assume

         A4: u in ( Support (m *' p));

        then

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

        u9 in { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support p) } by A2, A4;

        then

        consider s,t be Element of ( Bags n) such that

         A5: u9 = (s + t) & s in ( Support m) and

         A6: t in ( Support p);

        u9 = (( term m) + t) by A1, A5, TARSKI:def 1;

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

      end;

      now

        let u be object;

        assume u in { (( term m) + b) where b be Element of ( Bags n) : b in ( Support p) };

        then ex t be Element of ( Bags n) st u = (( term m) + t) & t in ( Support p);

        hence u in ( Support (m *' p)) by Th8;

      end;

      hence thesis by A3, TARSKI: 2;

    end;

    theorem :: GROEB_3:10

    

     Th10: for n be Ordinal, L be add-associative right_complementable left_zeroed right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, m be non-zero Monomial of n, L holds ( card ( Support p)) = ( card ( Support (m *' p)))

    proof

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

      defpred P[ object, object] means $2 = (( term m) + ( In ($1,( Bags n))));

      set T = the admissible connected TermOrder of n;

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

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

      then

       A1: ( Support m) = {( term m)} by POLYNOM7: 7;

      

       A2: for x be object st x in ( Support p) holds ex y be object st y in ( Support (m *' p)) & P[x, y]

      proof

        let x be object;

        assume

         A3: x in ( Support p);

        then

        reconsider x9 = x as Element of ( Bags n);

        (( term m) + x9) in ( Support (m *' p)) by A3, Th8;

        hence thesis;

      end;

      consider f be Function of ( Support p), ( Support (m *' p)) such that

       A5: for x be object st x in ( Support p) holds P[x, (f . x)] from FUNCT_2:sch 1( A2);

       A6:

      now

        assume

         A7: ( Support (m *' p)) = {} ;

        now

          assume ( Support p) <> {} ;

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

          then

          reconsider p9 = p as non-zero Polynomial of n, L by POLYNOM7:def 1;

          (( HT (m,T)) + ( HT (p9,T))) in ( Support (m *' p9)) by TERMORD: 29;

          hence contradiction by A7;

        end;

        hence ( Support p) = {} ;

      end;

      then

       A8: ( Support p) c= ( dom f) by FUNCT_2:def 1;

      

       A9: ( Support (m *' p)) c= { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support p) } by TERMORD: 30;

       A10:

      now

        let u be object;

        assume

         A11: u in ( Support (m *' p));

        then

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

        u9 in { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support p) } by A9, A11;

        then

        consider s,t be Element of ( Bags n) such that

         A12: u9 = (s + t) & s in ( Support m) and

         A13: t in ( Support p);

        

         A14: t in ( dom f) by A6, A13, FUNCT_2:def 1;

        

         A15: t = ( In (t,( Bags n)));

        u9 = (( term m) + t) by A1, A12, TARSKI:def 1;

        then u9 = (f . t) by A5, A13, A15;

        hence u in (f .: ( Support p)) by A14, FUNCT_1:def 6;

      end;

      now

        let x1,x2 be object;

        assume that

         A16: x1 in ( Support p) and

         A17: x2 in ( Support p) and

         A18: (f . x1) = (f . x2);

        reconsider x19 = x1, x29 = x2 as Element of ( Bags n) by A16, A17;

        

         A19: x29 = ( In (x29,( Bags n)));

        x19 = ( In (x19,( Bags n)));

        

        then (( term m) + x19) = (f . x29) by A5, A16, A18

        .= (( term m) + x29) by A5, A17, A19;

        

        hence x1 = ((x29 + ( term m)) -' ( term m)) by PRE_POLY: 48

        .= x2 by PRE_POLY: 48;

      end;

      then f is one-to-one by A6, FUNCT_2: 19;

      then

       A20: (( Support p),(f .: ( Support p))) are_equipotent by A8, CARD_1: 33;

      for u be object holds u in (f .: ( Support p)) implies u in ( Support (m *' p));

      then (f .: ( Support p)) = ( Support (m *' p)) by A10, TARSKI: 2;

      hence thesis by A20, CARD_1: 5;

    end;

    

     Lm1: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, g be object, P be Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) reduces (f,g) implies g is Polynomial of n, L

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, f be Polynomial of n, L, g be object, P be Subset of ( Polynom-Ring (n,L));

      set R = ( PolyRedRel (P,T));

      assume R reduces (f,g);

      then

      consider p be RedSequence of R such that

       A1: (p . 1) = f and

       A2: (p . ( len p)) = g by REWRITE1:def 3;

      reconsider l = (( len p) - 1) as Element of NAT by INT_1: 5, NAT_1: 14;

      

       A3: 1 <= ( len p) by NAT_1: 14;

      set h = (p . l);

      1 <= (l + 1) by NAT_1: 12;

      then

       A4: (l + 1) in ( dom p) by FINSEQ_3: 25;

      per cases ;

        suppose ( len p) = 1;

        hence thesis by A1, A2;

      end;

        suppose ( len p) <> 1;

        then ( 0 + 1) < (l + 1) by A3, XXREAL_0: 1;

        then

         A5: 1 <= l by NAT_1: 13;

        l <= (l + 1) by NAT_1: 13;

        then l in ( dom p) by A5, FINSEQ_3: 25;

        then [h, g] in R by A2, A4, REWRITE1:def 2;

        then

        consider h9,g9 be object such that

         A6: [h, g] = [h9, g9] and h9 in ( NonZero ( Polynom-Ring (n,L))) and

         A7: g9 in the carrier of ( Polynom-Ring (n,L)) by RELSET_1: 2;

        g = g9 by A6, XTUPLE_0: 1;

        hence thesis by A7, POLYNOM1:def 11;

      end;

    end;

    theorem :: GROEB_3:11

    

     Th11: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed non trivial addLoopStr holds ( Red (( 0_ (n,L)),T)) = ( 0_ (n,L))

    proof

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

      set e = ( 0_ (n,L)), h = ( HM (e,T));

      ( HC (h,T)) = ( HC (e,T)) by TERMORD: 27

      .= (e . ( HT (e,T))) by TERMORD:def 7

      .= ( 0. L) by POLYNOM1: 22;

      then h = ( 0_ (n,L)) by TERMORD: 17;

      

      hence ( Red (e,T)) = (e - ( 0_ (n,L))) by TERMORD:def 9

      .= ( 0_ (n,L)) by POLYRED: 4;

    end;

    theorem :: GROEB_3:12

    

     Th12: for n be Ordinal, L be Abelian add-associative right_zeroed right_complementable commutative well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L holds (p - q) = ( 0_ (n,L)) implies p = q

    proof

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

      assume (p - q) = ( 0_ (n,L));

      

      hence q = (q + (p - q)) by POLYNOM1: 23

      .= (q + (p + ( - q))) by POLYNOM1:def 7

      .= ((q + ( - q)) + p) by POLYNOM1: 21

      .= (( 0_ (n,L)) + p) by POLYRED: 3

      .= p by POLYRED: 2;

    end;

    theorem :: GROEB_3:13

    

     Th13: for X be set, L be add-associative right_zeroed right_complementable non empty addLoopStr holds ( - ( 0_ (X,L))) = ( 0_ (X,L))

    proof

      let X be set, L be add-associative right_zeroed right_complementable non empty addLoopStr;

      set o = ( - ( 0_ (X,L))), e = ( 0_ (X,L));

       A1:

      now

        let x be object;

        assume x in ( dom o);

        then

        reconsider b = x as bag of X;

        (o . b) = ( - (e . b)) by POLYNOM1: 17

        .= ( - ( 0. L)) by POLYNOM1: 22

        .= ( 0. L) by RLVECT_1: 12

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

        hence (o . x) = (e . x);

      end;

      ( dom o) = ( Bags X) by FUNCT_2:def 1

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

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: GROEB_3:14

    

     Th14: for X be set, L be add-associative right_zeroed right_complementable non empty addLoopStr, f be Series of X, L holds (( 0_ (X,L)) - f) = ( - f)

    proof

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

      set p = (( 0_ (X,L)) - f);

       A1:

      now

        let x be object;

        assume x in ( dom p);

        then

        reconsider b = x as Element of ( Bags X);

        (p . b) = ((( 0_ (X,L)) + ( - f)) . b) by POLYNOM1:def 7

        .= ((( 0_ (X,L)) . b) + (( - f) . b)) by POLYNOM1: 15

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

        .= (( - f) . b) by ALGSTR_1:def 2;

        hence (p . x) = (( - f) . x);

      end;

      ( dom p) = ( Bags X) by FUNCT_2:def 1

      .= ( dom ( - f)) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: GROEB_3:15

    

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

    proof

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

      

      thus (p - ( Red (p,T))) = ((( HM (p,T)) + ( Red (p,T))) - ( Red (p,T))) by TERMORD: 38

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

      .= (( HM (p,T)) + (( Red (p,T)) + ( - ( Red (p,T))))) by POLYNOM1: 21

      .= (( HM (p,T)) + ( 0_ (n,L))) by POLYRED: 3

      .= ( HM (p,T)) by POLYNOM1: 23;

    end;

    registration

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

      cluster ( Support p) -> finite;

      coherence by POLYNOM1:def 5;

    end

    definition

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

      :: original: {

      redefine

      func {p,q} -> Subset of ( Polynom-Ring (n,L)) ;

      coherence

      proof

        now

          let u be object;

          assume

           A1: u in {p, q};

          now

            per cases by A1, TARSKI:def 2;

              case u = p;

              hence u in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            end;

              case u = q;

              hence u in the carrier of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            end;

          end;

          hence u in the carrier of ( Polynom-Ring (n,L));

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    begin

    definition

      let X be set, L be non empty ZeroStr, s be Series of X, L, Y be Subset of ( Bags X);

      :: GROEB_3:def1

      func s | Y -> Series of X, L equals (s +* ((( Support s) \ Y) --> ( 0. L)));

      coherence

      proof

        set m = ((( Support s) \ Y) --> ( 0. L));

        set r = (s +* m);

         A1:

        now

          let x be object;

          assume x in ( Bags X);

          then

          reconsider x9 = x as Element of ( Bags X);

          now

            per cases ;

              case

               A2: x9 in ( dom m);

              

              then (r . x9) = (m . x9) by FUNCT_4: 13

              .= ( 0. L) by A2, FUNCOP_1: 7;

              hence (r . x) in the carrier of L;

            end;

              case not x in ( dom m);

              then (r . x9) = (s . x9) by FUNCT_4: 11;

              hence (r . x) in the carrier of L;

            end;

          end;

          hence (r . x) in the carrier of L;

        end;

        now

          let u be object;

          assume u in (( Support s) \ Y);

          then u in ( Support s) by XBOOLE_0:def 5;

          hence u in ( Bags X);

        end;

        then

         A3: (( Support s) \ Y) c= ( Bags X);

        ( dom s) = ( Bags X) & ( dom m) = (( Support s) \ Y) by FUNCT_2:def 1;

        then ( dom r) = (( Bags X) \/ (( Support s) \ Y)) by FUNCT_4:def 1;

        hence thesis by A3, A1, FUNCT_2: 3, XBOOLE_1: 12;

      end;

    end

    

     Lm2: for X be set, L be non empty ZeroStr, s be Series of X, L, Y be Subset of ( Bags X) holds ( Support (s | Y)) c= ( Support s)

    proof

      let X be set, L be non empty ZeroStr, s be Series of X, L, Y be Subset of ( Bags X);

      set m = ((( Support s) \ Y) --> ( 0. L));

      set r = (s +* m);

      let u be object;

      assume

       A1: u in ( Support (s | Y));

      then

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

      

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

      now

        per cases ;

          case u9 in ( dom m);

          hence u9 in ( Support s) by XBOOLE_0:def 5;

        end;

          case not u9 in ( dom m);

          hence (s . u9) <> ( 0. L) by A2, FUNCT_4: 11;

        end;

      end;

      hence thesis by POLYNOM1:def 4;

    end;

    registration

      let n be Ordinal, L be non empty ZeroStr, p be Polynomial of n, L, Y be Subset of ( Bags n);

      cluster (p | Y) -> finite-Support;

      coherence

      proof

        ( Support p) is finite by POLYNOM1:def 5;

        then ( Support (p | Y)) is finite by Lm2, FINSET_1: 1;

        hence thesis by POLYNOM1:def 5;

      end;

    end

    theorem :: GROEB_3:16

    

     Th16: for X be set, L be non empty ZeroStr, s be Series of X, L, Y be Subset of ( Bags X) holds ( Support (s | Y)) = (( Support s) /\ Y) & for b be bag of X st b in ( Support (s | Y)) holds ((s | Y) . b) = (s . b)

    proof

      let X be set, L be non empty ZeroStr, s be Series of X, L, Y be Subset of ( Bags X);

      set m = ((( Support s) \ Y) --> ( 0. L));

      set r = (s +* m);

       A1:

      now

        let u be object;

        assume

         A2: u in ( Support (s | Y));

        then

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

         A3:

        now

          assume

           A4: u9 in ( dom m);

          

          then (r . u9) = (m . u9) by FUNCT_4: 13

          .= ( 0. L) by A4, FUNCOP_1: 7;

          hence contradiction by A2, POLYNOM1:def 4;

        end;

        (r . u9) <> ( 0. L) by A2, POLYNOM1:def 4;

        then (s . u9) <> ( 0. L) by A3, FUNCT_4: 11;

        then

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

        ( dom m) = (( Support s) \ Y) by FUNCOP_1: 13;

        then u9 in Y by A3, A5, XBOOLE_0:def 5;

        hence u in (( Support s) /\ Y) by A5, XBOOLE_0:def 4;

      end;

      

       A6: ( dom m) = (( Support s) \ Y) by FUNCOP_1: 13;

      now

        let u be object;

        assume

         A7: u in (( Support s) /\ Y);

        then

         A8: u in ( Support s) by XBOOLE_0:def 4;

        then

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

        u in Y by A7, XBOOLE_0:def 4;

        then not u in (( Support s) \ Y) by XBOOLE_0:def 5;

        then (r . u9) = (s . u9) by A6, FUNCT_4: 11;

        then (r . u9) <> ( 0. L) by A8, POLYNOM1:def 4;

        hence u in ( Support (s | Y)) by POLYNOM1:def 4;

      end;

      hence

       A9: ( Support (s | Y)) = (( Support s) /\ Y) by A1, TARSKI: 2;

      now

        let b be bag of X;

        assume b in ( Support (s | Y));

        then b in Y by A9, XBOOLE_0:def 4;

        then not b in ( dom m) by XBOOLE_0:def 5;

        hence ((s | Y) . b) = (s . b) by FUNCT_4: 11;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:17

    for X be set, L be non empty ZeroStr, s be Series of X, L, Y be Subset of ( Bags X) holds ( Support (s | Y)) c= ( Support s) by Lm2;

    theorem :: GROEB_3:18

    for X be set, L be non empty ZeroStr, s be Series of X, L holds (s | ( Support s)) = s & (s | ( {} ( Bags X))) = ( 0_ (X,L))

    proof

      let X be set, L be non empty ZeroStr, s be Series of X, L;

      set r = (s | ( Support s));

      set e = (s | ( {} ( Bags X)));

      r = (s +* ( {} --> ( 0. L))) & ( dom ( {} --> ( 0. L))) = {} by XBOOLE_1: 37;

      

      hence r = (s +* {} )

      .= s;

      

       A1: ( dom (( Support s) --> ( 0. L))) = ( Support s) by FUNCOP_1: 13;

       A2:

      now

        let u be object;

        assume u in ( dom e);

        then

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

        now

          per cases ;

            case

             A3: u9 in ( Support s);

            

            then (e . u9) = ((( Support s) --> ( 0. L)) . u9) by A1, FUNCT_4: 13

            .= ( 0. L) by A3, FUNCOP_1: 7;

            hence (e . u9) = (( 0_ (X,L)) . u9) by POLYNOM1: 22;

          end;

            case

             A4: not u9 in ( Support s);

            then (e . u9) = (s . u9) by A1, FUNCT_4: 11;

            then (e . u9) = ( 0. L) by A4, POLYNOM1:def 4;

            hence (e . u9) = (( 0_ (X,L)) . u9) by POLYNOM1: 22;

          end;

        end;

        hence (e . u) = (( 0_ (X,L)) . u);

      end;

      ( dom e) = ( Bags X) by FUNCT_2:def 1

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

      hence thesis by A2, FUNCT_1: 2;

    end;

    definition

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

      :: GROEB_3:def2

      func Upper_Support (p,T,i) -> finite Subset of ( Bags n) means

      : Def2: it c= ( Support p) & ( card it ) = i & for b,b9 be bag of n st b in it & b9 in ( Support p) & b <= (b9,T) holds b9 in it ;

      existence

      proof

        defpred P[ Nat] means $1 > ( card ( Support p)) or ex M be finite Subset of ( Bags n) st M c= ( Support p) & ( card M) = $1 & for b,b9 be bag of n st b in M & b9 in ( Support p) & b <= (b9,T) holds b9 in M;

         A2:

        now

          let k be Nat;

          assume

           A3: P[k];

          (k + 1) > ( card ( Support p)) or ex M be finite Subset of ( Bags n) st M c= ( Support p) & ( card M) = (k + 1) & for b,b9 be bag of n st b in M & b9 in ( Support p) & b <= (b9,T) holds b9 in M

          proof

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

            assume

             A4: not (k + 1) > ( card ( Support p));

            k <= (k + 1) by NAT_1: 11;

            then

            consider M1 be finite Subset of ( Bags n) such that

             A5: M1 c= ( Support p) and

             A6: ( card M1) = k and

             A7: for b,b9 be bag of n st b in M1 & b9 in ( Support p) & b <= (b9,T) holds b9 in M1 by A3, A4, XXREAL_0: 2;

            set G = (( Support p) \ M1);

            now

              let u be object;

              assume u in G;

              then u in ( Support p) by XBOOLE_0:def 5;

              hence u in ( Bags n);

            end;

            then

            reconsider G as Subset of ( Bags n) by TARSKI:def 3;

            

             A8: for u be object holds u in M1 implies u in ( Support p) by A5;

            now

              assume G = {} ;

              then ( Support p) c= M1 by XBOOLE_1: 37;

              then for u be object holds u in ( Support p) implies u in M1;

              then ( card ( Support p)) = k by A6, A8, TARSKI: 2;

              hence contradiction by A4, NAT_1: 16;

            end;

            then

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

            consider x be Element of R such that

             A9: x in G and

             A10: x is_maximal_wrt (G,the InternalRel of R) by BAGORDER: 6;

            reconsider b = x as bag of n;

            set M = (M1 \/ {b});

            now

              let u be object;

              assume u in {b};

              then u = b by TARSKI:def 1;

              hence u in ( Bags n);

            end;

            then {b} c= ( Bags n);

            then M c= (( Bags n) \/ ( Bags n)) by XBOOLE_1: 13;

            then

            reconsider M as finite Subset of ( Bags n);

            now

              let u be object;

              assume

               A11: u in M;

              now

                per cases by A11, XBOOLE_0:def 3;

                  case u in M1;

                  hence u in ( Support p) by A5;

                end;

                  case u in {b};

                  then u in G by A9, TARSKI:def 1;

                  hence u in ( Support p) by XBOOLE_0:def 5;

                end;

              end;

              hence u in ( Support p);

            end;

            then

             A12: M c= ( Support p);

             A13:

            now

              let b9 be bag of n;

              assume

               A14: b9 in G;

              now

                per cases ;

                  case b9 = b;

                  hence b9 <= (b,T) by TERMORD: 6;

                end;

                  case b9 <> b;

                  then not [b, b9] in T by A10, A14, WAYBEL_4:def 23;

                  then not b <= (b9,T) by TERMORD:def 2;

                  then b9 < (b,T) by TERMORD: 5;

                  hence b9 <= (b,T) by TERMORD:def 3;

                end;

              end;

              hence b9 <= (b,T);

            end;

             A15:

            now

              let b1,b2 be bag of n;

              assume that

               A16: b1 in M and

               A17: b2 in ( Support p) and

               A18: b1 <= (b2,T);

              now

                per cases by A16, XBOOLE_0:def 3;

                  case b1 in M1;

                  then b2 in M1 by A7, A17, A18;

                  hence b2 in M by XBOOLE_0:def 3;

                end;

                  case b1 in {b};

                  then

                   A19: b1 = b by TARSKI:def 1;

                  per cases ;

                    suppose b2 = b1;

                    hence b2 in M by A16;

                  end;

                    suppose b2 <> b1;

                    then

                     A20: b1 < (b2,T) by A18, TERMORD:def 3;

                     not b2 in G by A20, TERMORD: 5, A13, A19;

                    then b2 in M1 by A17, XBOOLE_0:def 5;

                    hence b2 in M by XBOOLE_0:def 3;

                  end;

                end;

              end;

              hence b2 in M;

            end;

             not b in M1 by A9, XBOOLE_0:def 5;

            then ( card M) = (k + 1) by A6, CARD_2: 41;

            hence thesis by A12, A15;

          end;

          hence P[(k + 1)];

        end;

        ex M be finite Subset of ( Bags n) st M c= ( Support p) & ( card M) = 0 & for b,b9 be bag of n st b in M & b9 in ( Support p) & b <= (b9,T) holds b9 in M

        proof

          set M = ( {} ( Bags n));

          take M;

          thus thesis;

        end;

        then

         A21: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A21, A2);

        hence thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be finite Subset of ( Bags n);

        assume that

         A22: F1 c= ( Support p) and

         A23: ( card F1) = i and

         A24: for b,b9 be bag of n st b in F1 & b9 in ( Support p) & b <= (b9,T) holds b9 in F1;

        assume that

         A25: F2 c= ( Support p) and

         A26: ( card F2) = i and

         A27: for b,b9 be bag of n st b in F2 & b9 in ( Support p) & b <= (b9,T) holds b9 in F2;

        now

          let u be object;

          assume

           A28: u in F1;

          then

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

          now

            assume

             A29: not u9 in F2;

            now

              let x be object;

              assume

               A30: x in F2;

              then

              reconsider x9 = x as Element of ( Bags n);

              now

                per cases ;

                  case u9 <= (x9,T);

                  hence x9 in F1 by A24, A25, A28, A30;

                end;

                  case not u9 <= (x9,T);

                  then x9 < (u9,T) by TERMORD: 5;

                  then x9 <= (u9,T) by TERMORD:def 3;

                  hence x9 in F1 by A22, A27, A28, A29, A30;

                end;

              end;

              hence x in F1;

            end;

            then F2 c= F1;

            then F2 c< F1 by A28, A29, XBOOLE_0:def 8;

            hence contradiction by A23, A26, CARD_2: 48;

          end;

          hence u in F2;

        end;

        then F1 c= F2;

        hence thesis by A23, A26, CARD_2: 102;

      end;

    end

    definition

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

      :: GROEB_3:def3

      func Lower_Support (p,T,i) -> finite Subset of ( Bags n) equals (( Support p) \ ( Upper_Support (p,T,i)));

      coherence

      proof

        (( Support p) \ ( Upper_Support (p,T,i))) c= ( Support p) by XBOOLE_1: 36;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    theorem :: GROEB_3:19

    

     Th19: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds (( Upper_Support (p,T,i)) \/ ( Lower_Support (p,T,i))) = ( Support p) & (( Upper_Support (p,T,i)) /\ ( Lower_Support (p,T,i))) = {}

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      set M = (( Upper_Support (p,T,i)) /\ (( Support p) \ ( Upper_Support (p,T,i))));

      assume i <= ( card ( Support p));

      then

       A1: ( Upper_Support (p,T,i)) c= ( Support p) by Def2;

      

      thus (( Upper_Support (p,T,i)) \/ ( Lower_Support (p,T,i))) = (( Upper_Support (p,T,i)) \/ ( Support p)) by XBOOLE_1: 39

      .= ( Support p) by A1, XBOOLE_1: 12;

      now

        set x = the Element of M;

        assume M <> {} ;

        then x in ( Upper_Support (p,T,i)) & x in (( Support p) \ ( Upper_Support (p,T,i))) by XBOOLE_0:def 4;

        hence contradiction by XBOOLE_0:def 5;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:20

    

     Th20: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds for b,b9 be bag of n st b in ( Upper_Support (p,T,i)) & b9 in ( Lower_Support (p,T,i)) holds b9 < (b,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      assume

       A1: i <= ( card ( Support p));

      let b,b9 be bag of n;

      assume that

       A2: b in ( Upper_Support (p,T,i)) and

       A3: b9 in ( Lower_Support (p,T,i));

      

       A4: ( Lower_Support (p,T,i)) c= ( Support p) by XBOOLE_1: 36;

      now

        assume b <= (b9,T);

        then b9 in ( Upper_Support (p,T,i)) by A1, A2, A3, A4, Def2;

        then b9 in (( Upper_Support (p,T,i)) /\ ( Lower_Support (p,T,i))) by A3, XBOOLE_0:def 4;

        hence contradiction by A1, Th19;

      end;

      hence thesis by TERMORD: 5;

    end;

    theorem :: GROEB_3:21

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L holds ( Upper_Support (p,T, 0 )) = {} & ( Lower_Support (p,T, 0 )) = ( Support p)

    proof

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

      set u = ( Upper_Support (p,T, 0 ));

       0 <= ( card ( Support p));

      then ( card u) = 0 by Def2;

      hence u = {} ;

      hence thesis;

    end;

    theorem :: GROEB_3:22

    

     Th22: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L holds ( Upper_Support (p,T,( card ( Support p)))) = ( Support p) & ( Lower_Support (p,T,( card ( Support p)))) = {}

    proof

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

      set u = ( Upper_Support (p,T,( card ( Support p))));

      u c= ( Support p) & ( card u) = ( card ( Support p)) by Def2;

      hence u = ( Support p) by CARD_2: 102;

      hence thesis by XBOOLE_1: 37;

    end;

    theorem :: GROEB_3:23

    

     Th23: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non trivial addLoopStr, p be non-zero Polynomial of n, L, i be Element of NAT st 1 <= i & i <= ( card ( Support p)) holds ( HT (p,T)) in ( Upper_Support (p,T,i))

    proof

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

      assume that

       A1: 1 <= i and

       A2: i <= ( card ( Support p));

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

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

      then

       A3: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

      set u = ( Upper_Support (p,T,i));

      set x = the Element of u;

      

       A4: u <> {} by A1, A2, Def2, CARD_1: 27;

      then

       A5: x in u;

      then

      reconsider x9 = x as Element of ( Bags n);

      u c= ( Support p) by A2, Def2;

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

      hence thesis by A2, A4, A3, Def2;

    end;

    theorem :: GROEB_3:24

    

     Th24: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds ( Lower_Support (p,T,i)) c= ( Support p) & ( card ( Lower_Support (p,T,i))) = (( card ( Support p)) - i) & for b,b9 be bag of n st b in ( Lower_Support (p,T,i)) & b9 in ( Support p) & b9 <= (b,T) holds b9 in ( Lower_Support (p,T,i))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      assume

       A1: i <= ( card ( Support p));

      set l = ( Lower_Support (p,T,i));

      thus l c= ( Support p) by XBOOLE_1: 36;

      ( Upper_Support (p,T,i)) c= ( Support p) by A1, Def2;

      

      hence ( card l) = (( card ( Support p)) - ( card ( Upper_Support (p,T,i)))) by CARD_2: 44

      .= (( card ( Support p)) - i) by A1, Def2;

      now

        let b,b9 be bag of n;

        assume that

         A2: b in ( Lower_Support (p,T,i)) and

         A3: b9 in ( Support p) and

         A4: b9 <= (b,T);

        

         A5: b9 in (( Upper_Support (p,T,i)) \/ ( Lower_Support (p,T,i))) by A1, A3, Th19;

        now

          assume not b9 in ( Lower_Support (p,T,i));

          then b9 in ( Upper_Support (p,T,i)) by A5, XBOOLE_0:def 3;

          then b < (b9,T) by A1, A2, Th20;

          hence contradiction by A4, TERMORD: 5;

        end;

        hence b9 in ( Lower_Support (p,T,i));

      end;

      hence thesis;

    end;

    definition

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

      :: GROEB_3:def4

      func Up (p,T,i) -> Polynomial of n, L equals (p | ( Upper_Support (p,T,i)));

      coherence ;

      :: GROEB_3:def5

      func Low (p,T,i) -> Polynomial of n, L equals (p | ( Lower_Support (p,T,i)));

      coherence ;

    end

    

     Lm3: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds ( Support (p | ( Upper_Support (p,T,i)))) = ( Upper_Support (p,T,i)) & ( Support (p | ( Lower_Support (p,T,i)))) = ( Lower_Support (p,T,i))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      set u = ( Upper_Support (p,T,i)), pu = (p | ( Upper_Support (p,T,i)));

      set l = ( Lower_Support (p,T,i)), pl = (p | ( Lower_Support (p,T,i)));

      assume i <= ( card ( Support p));

      then

       A1: u c= ( Support p) by Def2;

      ( Support pu) = (( Support p) /\ u) by Th16;

      hence ( Support pu) = u by A1, XBOOLE_1: 28;

      ( Support pl) = (( Support p) /\ l) by Th16;

      hence thesis by XBOOLE_1: 28, XBOOLE_1: 36;

    end;

    theorem :: GROEB_3:25

    for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds ( Support ( Up (p,T,i))) = ( Upper_Support (p,T,i)) & ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by Lm3;

    theorem :: GROEB_3:26

    

     Th26: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds ( Support ( Up (p,T,i))) c= ( Support p) & ( Support ( Low (p,T,i))) c= ( Support p)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      assume

       A1: i <= ( card ( Support p));

      then ( Support (p | ( Upper_Support (p,T,i)))) = ( Upper_Support (p,T,i)) & ( Support (p | ( Lower_Support (p,T,i)))) = ( Lower_Support (p,T,i)) by Lm3;

      hence thesis by A1, Def2, Th24;

    end;

    theorem :: GROEB_3:27

    

     Th27: 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, i be Element of NAT st 1 <= i & i <= ( card ( Support p)) holds ( Support ( Low (p,T,i))) c= ( Support ( Red (p,T)))

    proof

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

      assume that

       A1: 1 <= i and

       A2: i <= ( card ( Support p));

      ( Support p) <> {} by A1, A2;

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

      then

      reconsider p as non-zero Polynomial of n, L by POLYNOM7:def 1;

      set sl = ( Lower_Support (p,T,i));

       A3:

      now

        assume

         A4: ( HT (p,T)) in sl;

        ( HT (p,T)) in ( Upper_Support (p,T,i)) by A1, A2, Th23;

        then ( HT (p,T)) in (( Upper_Support (p,T,i)) /\ sl) by A4, XBOOLE_0:def 4;

        hence contradiction by A2, Th19;

      end;

      now

        set u = the Element of ( {( HT (p,T))} /\ sl);

        assume ( {( HT (p,T))} /\ sl) <> {} ;

        then u in {( HT (p,T))} & u in sl by XBOOLE_0:def 4;

        hence contradiction by A3, TARSKI:def 1;

      end;

      then {( HT (p,T))} misses sl by XBOOLE_0:def 7;

      

      then

       A5: (sl \ {( HT (p,T))}) = sl by XBOOLE_1: 83

      .= ( Support ( Low (p,T,i))) by A2, Lm3;

      (( Support ( Low (p,T,i))) \ {( HT (p,T))}) c= (( Support p) \ {( HT (p,T))}) by A2, Th26, XBOOLE_1: 33;

      then (( Support ( Low (p,T,i))) \ {( HT (p,T))}) c= ( Support ( Red (p,T))) by TERMORD: 36;

      hence thesis by A2, A5, Lm3;

    end;

    theorem :: GROEB_3:28

    

     Th28: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds for b be bag of n st b in ( Support p) holds (b in ( Support ( Up (p,T,i))) or b in ( Support ( Low (p,T,i)))) & not (b in (( Support ( Up (p,T,i))) /\ ( Support ( Low (p,T,i)))))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      assume

       A1: i <= ( card ( Support p));

      let b be bag of n;

      assume

       A2: b in ( Support p);

      ( Support p) = (( Upper_Support (p,T,i)) \/ ( Lower_Support (p,T,i))) by A1, Th19

      .= (( Support ( Up (p,T,i))) \/ ( Lower_Support (p,T,i))) by A1, Lm3

      .= (( Support ( Up (p,T,i))) \/ ( Support ( Low (p,T,i)))) by A1, Lm3;

      hence b in ( Support ( Up (p,T,i))) or b in ( Support ( Low (p,T,i))) by A2, XBOOLE_0:def 3;

      ( Support ( Up (p,T,i))) = ( Upper_Support (p,T,i)) & ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by A1, Lm3;

      hence thesis by A1, Th19;

    end;

    theorem :: GROEB_3:29

    

     Th29: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds for b,b9 be bag of n st b in ( Support ( Low (p,T,i))) & b9 in ( Support ( Up (p,T,i))) holds b < (b9,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      assume

       A1: i <= ( card ( Support p));

      let b,b9 be bag of n;

      assume

       A2: b in ( Support ( Low (p,T,i))) & b9 in ( Support ( Up (p,T,i)));

      ( Support ( Up (p,T,i))) = ( Upper_Support (p,T,i)) & ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by A1, Lm3;

      hence thesis by A1, A2, Th20;

    end;

    theorem :: GROEB_3:30

    

     Th30: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st 1 <= i & i <= ( card ( Support p)) holds ( HT (p,T)) in ( Support ( Up (p,T,i)))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      assume that

       A1: 1 <= i and

       A2: i <= ( card ( Support p));

      ( Support p) <> {} by A1, A2;

      then

       A3: ( HT (p,T)) in ( Support p) by TERMORD:def 6;

      set u = ( Up (p,T,i));

      set x = the Element of ( Support u);

      

       A4: ( Support u) = ( Upper_Support (p,T,i)) by A2, Lm3;

      then ( card ( Support u)) <> 0 by A1, A2, Def2;

      then

       A5: ( Support u) <> {} ;

      then

       A6: x in ( Support u);

      then

      reconsider x as Element of ( Bags n);

      ( Support u) c= ( Support p) by A2, A4, Def2;

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

      hence thesis by A2, A4, A5, A3, Def2;

    end;

    theorem :: GROEB_3:31

    

     Th31: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds for b be bag of n st b in ( Support ( Low (p,T,i))) holds (( Low (p,T,i)) . b) = (p . b) & (( Up (p,T,i)) . b) = ( 0. L)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      set l = ( Lower_Support (p,T,i));

      assume

       A1: i <= ( card ( Support p));

      then

       A2: (l /\ ( Upper_Support (p,T,i))) = {} by Th19;

      let b be bag of n;

      assume

       A3: b in ( Support ( Low (p,T,i)));

      hence (( Low (p,T,i)) . b) = (p . b) by Th16;

      b in l by A1, A3, Lm3;

      then not b in ( Upper_Support (p,T,i)) by A2, XBOOLE_0:def 4;

      then

       A4: not b in ( Support ( Up (p,T,i))) by A1, Lm3;

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

      hence thesis by A4, POLYNOM1:def 4;

    end;

    theorem :: GROEB_3:32

    

     Th32: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds for b be bag of n st b in ( Support ( Up (p,T,i))) holds (( Up (p,T,i)) . b) = (p . b) & (( Low (p,T,i)) . b) = ( 0. L)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      set u = ( Upper_Support (p,T,i));

      assume

       A1: i <= ( card ( Support p));

      then

       A2: (u /\ ( Lower_Support (p,T,i))) = {} by Th19;

      let b be bag of n;

      assume

       A3: b in ( Support ( Up (p,T,i)));

      hence (( Up (p,T,i)) . b) = (p . b) by Th16;

      b in u by A1, A3, Lm3;

      then not b in ( Lower_Support (p,T,i)) by A2, XBOOLE_0:def 4;

      then

       A4: not b in ( Support ( Low (p,T,i))) by A1, Lm3;

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

      hence thesis by A4, POLYNOM1:def 4;

    end;

    theorem :: GROEB_3:33

    

     Th33: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds (( Up (p,T,i)) + ( Low (p,T,i))) = p

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      set u = (( Up (p,T,i)) + ( Low (p,T,i)));

      assume

       A1: i <= ( card ( Support p));

       A2:

      now

        let x be object;

        assume

         A3: x in ( Support p);

        then

        reconsider x9 = x as Element of ( Bags n);

        

         A4: (u . x9) = ((( Up (p,T,i)) . x9) + (( Low (p,T,i)) . x9)) by POLYNOM1: 15;

         A5:

        now

          per cases by A1, A3, Th28;

            case

             A6: x9 in ( Support ( Up (p,T,i)));

            

            hence (u . x9) = ((( Up (p,T,i)) . x9) + ( 0. L)) by A1, A4, Th32

            .= (( Up (p,T,i)) . x9) by RLVECT_1:def 4

            .= (p . x9) by A1, A6, Th32;

          end;

            case

             A7: x9 in ( Support ( Low (p,T,i)));

            

            hence (u . x9) = (( 0. L) + (( Low (p,T,i)) . x9)) by A1, A4, Th31

            .= (( Low (p,T,i)) . x9) by ALGSTR_1:def 2

            .= (p . x9) by A1, A7, Th31;

          end;

        end;

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

        hence x in ( Support u) by A5, POLYNOM1:def 4;

      end;

      now

        let x be object;

        ( Support ( Up (p,T,i))) c= ( Support p) & ( Support ( Low (p,T,i))) c= ( Support p) by A1, Th26;

        then ( Support u) c= (( Support ( Up (p,T,i))) \/ ( Support ( Low (p,T,i)))) & (( Support ( Up (p,T,i))) \/ ( Support ( Low (p,T,i)))) c= ( Support p) by POLYNOM1: 20, XBOOLE_1: 8;

        then

         A8: ( Support u) c= ( Support p);

        assume x in ( Support u);

        hence x in ( Support p) by A8;

      end;

      then

       A9: ( Support u) = ( Support p) by A2, TARSKI: 2;

       A10:

      now

        let x be object;

        assume x in ( dom p);

        then

        reconsider x9 = x as Element of ( Bags n);

        

         A11: (u . x9) = ((( Up (p,T,i)) . x9) + (( Low (p,T,i)) . x9)) by POLYNOM1: 15;

        now

          per cases ;

            case

             A12: x9 in ( Support p);

            now

              per cases by A1, A12, Th28;

                case

                 A13: x9 in ( Support ( Up (p,T,i)));

                

                hence (u . x9) = ((( Up (p,T,i)) . x9) + ( 0. L)) by A1, A11, Th32

                .= (( Up (p,T,i)) . x9) by RLVECT_1:def 4

                .= (p . x9) by A1, A13, Th32;

              end;

                case

                 A14: x9 in ( Support ( Low (p,T,i)));

                

                hence (u . x9) = (( 0. L) + (( Low (p,T,i)) . x9)) by A1, A11, Th31

                .= (( Low (p,T,i)) . x9) by ALGSTR_1:def 2

                .= (p . x9) by A1, A14, Th31;

              end;

            end;

            hence (p . x9) = (u . x9);

          end;

            case

             A15: not x9 in ( Support p);

            

            hence (p . x9) = ( 0. L) by POLYNOM1:def 4

            .= (u . x9) by A9, A15, POLYNOM1:def 4;

          end;

        end;

        hence (p . x) = (u . x);

      end;

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

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

      hence thesis by A10, FUNCT_1: 2;

    end;

    theorem :: GROEB_3:34

    

     Th34: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L holds ( Up (p,T, 0 )) = ( 0_ (n,L)) & ( Low (p,T, 0 )) = p

    proof

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

      set u = ( Up (p,T, 0 )), l = ( Low (p,T, 0 ));

      

       A1: 0 <= ( card ( Support p));

      then ( Support u) = ( Upper_Support (p,T, 0 )) by Lm3;

      then ( card ( Support u)) = 0 by A1, Def2;

      then ( Support u) = {} ;

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

      then (( 0_ (n,L)) + l) = p by A1, Th33;

      hence thesis by POLYRED: 2;

    end;

    theorem :: GROEB_3:35

    

     Th35: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, p be Polynomial of n, L holds ( Up (p,T,( card ( Support p)))) = p & ( Low (p,T,( card ( Support p)))) = ( 0_ (n,L))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable Abelian non empty doubleLoopStr, p be Polynomial of n, L;

      set u = ( Up (p,T,( card ( Support p)))), l = ( Low (p,T,( card ( Support p))));

      ( Support u) = (( Support p) /\ ( Upper_Support (p,T,( card ( Support p))))) by Th16;

      then

       A1: ( Support u) c= ( Support p) by XBOOLE_1: 17;

      

       A2: ( card ( Support u)) = ( card ( Upper_Support (p,T,( card ( Support p))))) by Lm3

      .= ( card ( Support p)) by Th22;

       A3:

      now

        let x be object;

        assume

         A4: x in ( Support p);

        now

          assume not x in ( Support u);

          then ( Support u) c< ( Support p) by A1, A4, XBOOLE_0:def 8;

          hence contradiction by A2, CARD_2: 48;

        end;

        hence x in ( Support u);

      end;

      for x be object holds x in ( Support u) implies x in ( Support p) by A1;

      then

       A5: ( Support u) = ( Support p) by A3, TARSKI: 2;

       A6:

      now

        let x be object;

        assume x in ( dom p);

        then

        reconsider x9 = x as Element of ( Bags n);

        now

          per cases ;

            case x in ( Support p);

            hence (p . x9) = (u . x9) by A5, Th16;

          end;

            case

             A7: not x in ( Support p);

            

            hence (p . x9) = ( 0. L) by POLYNOM1:def 4

            .= (u . x9) by A5, A7, POLYNOM1:def 4;

          end;

        end;

        hence (p . x) = (u . x);

      end;

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

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

      hence

       A8: p = u by A6, FUNCT_1: 2;

      

      thus ( 0_ (n,L)) = (p + ( - p)) by POLYRED: 3

      .= ((l + p) + ( - p)) by A8, Th33

      .= (l + (p + ( - p))) by POLYNOM1: 21

      .= (l + ( 0_ (n,L))) by POLYRED: 3

      .= l by POLYRED: 2;

    end;

    theorem :: GROEB_3:36

    

     Th36: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable Abelian non trivial doubleLoopStr, p be non-zero Polynomial of n, L holds ( Up (p,T,1)) = ( HM (p,T)) & ( Low (p,T,1)) = ( Red (p,T))

    proof

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

      set u = ( Up (p,T,1)), l = ( Low (p,T,1));

       A1:

      now

        assume ( card ( Support p)) < 1;

        then ( Support p) = {} by NAT_1: 14;

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

        hence contradiction by POLYNOM7:def 1;

      end;

      then ( Support u) = ( Upper_Support (p,T,1)) by Lm3;

      then ( card ( Support u)) = 1 by A1, Def2;

      then

      consider x be object such that

       A2: ( Support u) = {x} by CARD_2: 42;

      ( HT (p,T)) in {x} by A1, A2, Th30;

      then

       A3: ( Support u) = {( HT (p,T))} by A2, TARSKI:def 1;

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

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

      then

       A4: ( Support u) = ( Support ( HM (p,T))) by A3, TERMORD: 21;

       A5:

      now

        let x be object;

        assume x in ( dom ( HM (p,T)));

        then

        reconsider x9 = x as Element of ( Bags n);

        now

          per cases ;

            case

             A6: x in ( Support ( HM (p,T)));

            then x9 = ( HT (p,T)) by A3, A4, TARSKI:def 1;

            

            hence (( HM (p,T)) . x9) = (p . x9) by TERMORD: 18

            .= (u . x9) by A4, A6, Th16;

          end;

            case

             A7: not x in ( Support ( HM (p,T)));

            

            hence (( HM (p,T)) . x9) = ( 0. L) by POLYNOM1:def 4

            .= (u . x9) by A4, A7, POLYNOM1:def 4;

          end;

        end;

        hence (( HM (p,T)) . x) = (u . x);

      end;

      ( dom ( HM (p,T))) = ( Bags n) by FUNCT_2:def 1

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

      hence ( HM (p,T)) = u by A5, FUNCT_1: 2;

      then

       A8: (( HM (p,T)) + l) = p by A1, Th33;

      

      thus ( Red (p,T)) = (p - ( HM (p,T))) by TERMORD:def 9

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

      .= (l + (( HM (p,T)) + ( - ( HM (p,T))))) by POLYNOM1: 21

      .= (l + ( 0_ (n,L))) by POLYRED: 3

      .= l by POLYRED: 2;

    end;

    registration

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

      cluster ( Up (p,T, 0 )) -> monomial-like;

      coherence

      proof

        ( Up (p,T, 0 )) = ( 0_ (n,L)) by Th34;

        hence thesis;

      end;

    end

    registration

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

      cluster ( Up (p,T,1)) -> non-zero monomial-like;

      coherence

      proof

        ( Up (p,T,1)) = ( HM (p,T)) by Th36;

        hence thesis;

      end;

      cluster ( Low (p,T,( card ( Support p)))) -> monomial-like;

      coherence

      proof

        ( Low (p,T,( card ( Support p)))) = ( 0_ (n,L)) by Th35;

        hence thesis;

      end;

    end

    theorem :: GROEB_3:37

    

     Th37: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non trivial addLoopStr, p be Polynomial of n, L, j be Element of NAT st j = (( card ( Support p)) - 1) holds ( Low (p,T,j)) is non-zero Monomial of n, L

    proof

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

      set l = ( Low (p,T,j));

      assume

       A1: j = (( card ( Support p)) - 1);

       A2:

      now

        assume j > ( card ( Support p));

        then ((( card ( Support p)) - 1) + 1) > (( card ( Support p)) + 1) by A1, XREAL_1: 8;

        then (( card ( Support p)) + ( - ( card ( Support p)))) > ((( card ( Support p)) + 1) + ( - ( card ( Support p)))) by XREAL_1: 8;

        hence contradiction;

      end;

      then ( Support l) = ( Lower_Support (p,T,j)) by Lm3;

      then ( card ( Support l)) = (( card ( Support p)) - (( card ( Support p)) - 1)) by A1, A2, Th24;

      then

      consider x be object such that

       A3: ( Support l) = {x} by CARD_2: 42;

      x in ( Support l) by A3, TARSKI:def 1;

      then

       A4: x is Element of ( Bags n);

      l <> ( 0_ (n,L)) by A3, POLYNOM7: 1;

      hence thesis by A3, A4, POLYNOM7: 6, POLYNOM7:def 1;

    end;

    theorem :: GROEB_3:38

    

     Th38: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i < ( card ( Support p)) holds ( HT (( Low (p,T,(i + 1))),T)) <= (( HT (( Low (p,T,i)),T)),T)

    proof

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

      set li = ( Low (p,T,i)), li1 = ( Low (p,T,(i + 1)));

      assume

       A1: i < ( card ( Support p));

      then ( Support li) = ( Lower_Support (p,T,i)) by Lm3;

      then

       A2: ( card ( Support li)) = (( card ( Support p)) - i) by A1, Th24;

      

       A3: (i + 1) <= ( card ( Support p)) by A1, NAT_1: 13;

      then

       A4: ( Support li1) = ( Lower_Support (p,T,(i + 1))) by Lm3;

      then

       A5: ( card ( Support li1)) = (( card ( Support p)) - (i + 1)) by A3, Th24;

      

       A6: ( Support li) c= ( Support p) by A1, Th26;

      now

        per cases ;

          case i = (( card ( Support p)) - 1);

          

          then ( card ( Support li1)) = (( card ( Support p)) - ( card ( Support p))) by A4, Th24

          .= 0 ;

          then ( Support li1) = {} ;

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

          hence thesis by TERMORD: 9;

        end;

          case i <> (( card ( Support p)) - 1);

          then ( card ( Lower_Support (p,T,(i + 1)))) <> 0 by A4, A5;

          then ( Lower_Support (p,T,(i + 1))) <> {} ;

          then

           A7: ( HT (( Low (p,T,(i + 1))),T)) in ( Lower_Support (p,T,(i + 1))) by A4, TERMORD:def 6;

          now

            assume ( HT (( Low (p,T,i)),T)) < (( HT (( Low (p,T,(i + 1))),T)),T);

            then

             A8: ( HT (( Low (p,T,i)),T)) <= (( HT (( Low (p,T,(i + 1))),T)),T) by TERMORD:def 3;

            now

              let u9 be object;

              assume

               A9: u9 in ( Support li);

              then

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

              u <= (( HT (( Low (p,T,i)),T)),T) by A9, TERMORD:def 6;

              hence u9 in ( Support li1) by A3, A6, A4, A7, A8, A9, Th24, TERMORD: 8;

            end;

            then ( Support li) c= ( Support li1);

            then (( card ( Support p)) + ( - i)) <= (( card ( Support p)) + ( - (i + 1))) by A2, A5, NAT_1: 43;

            then ( - i) <= ( - (i + 1)) by XREAL_1: 6;

            then (i + 1) <= i by XREAL_1: 24;

            then ((i + 1) - i) <= (i - i) by XREAL_1: 9;

            then 1 <= 0 ;

            hence contradiction;

          end;

          hence thesis by TERMORD: 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:39

    

     Th39: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st 0 < i & i < ( card ( Support p)) holds ( HT (( Low (p,T,i)),T)) < (( HT (p,T)),T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT ;

      assume that

       A1: 0 < i and

       A2: i < ( card ( Support p));

      set l = ( Low (p,T,i));

      now

        per cases ;

          case l = ( 0_ (n,L));

          then

           A3: ( card ( Support l)) = 0 by CARD_1: 27, POLYNOM7: 1;

          ( Support l) = ( Lower_Support (p,T,i)) by A2, Lm3;

          then ( 0 + i) = ((( card ( Support p)) - i) + i) by A2, A3, Th24;

          hence contradiction by A2;

        end;

          case

           A4: l <> ( 0_ (n,L));

          

           A5: ( Support ( Low (p,T,i))) c= ( Support p) by A2, Th26;

          

           A6: ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by A2, Lm3;

           A7:

          now

            assume

             A8: ( HT (p,T)) in ( Support l);

             A9:

            now

              let u be object;

              assume

               A10: u in ( Support p);

              then

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

              x <= (( HT (p,T)),T) by A10, TERMORD:def 6;

              hence u in ( Support l) by A2, A6, A8, A10, Th24;

            end;

            for u be object holds u in ( Support l) implies u in ( Support p) by A5;

            

            then ( card ( Support p)) = ( card ( Support l)) by A9, TARSKI: 2

            .= (( card ( Support p)) - i) by A2, A6, Th24;

            hence contradiction by A1;

          end;

          ( Support l) <> {} by A4, POLYNOM7: 1;

          then

           A11: ( HT (l,T)) in ( Support l) by TERMORD:def 6;

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

          hence thesis by A7, A11, TERMORD:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:40

    

     Th40: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, m be non-zero Monomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds for b be bag of n holds (( term m) + b) in ( Support ( Low ((m *' p),T,i))) iff b in ( Support ( Low (p,T,i)))

    proof

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

      set l = ( Low (p,T,i));

      assume

       A1: i <= ( card ( Support p));

      then

       A2: ( Support l) c= ( Support p) by Th26;

      

       A3: ( Support ( Up (p,T,i))) = ( Upper_Support (p,T,i)) by A1, Lm3;

      then

       A4: ( card ( Support ( Up (p,T,i)))) = i by A1, Def2;

      

       A5: ( Support ( Up (p,T,i))) c= ( Support p) by A1, Th26;

      

       A6: ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by A1, Lm3;

      let b be bag of n;

      

       A7: i <= ( card ( Support (m *' p))) by A1, Th10;

      then

       A8: ( Support ( Low ((m *' p),T,i))) = ( Lower_Support ((m *' p),T,i)) by Lm3;

      

       A9: ( Support ( Low ((m *' p),T,i))) c= ( Support (m *' p)) by A7, Th26;

      

       A10: ( Support ( Up ((m *' p),T,i))) c= ( Support (m *' p)) by A7, Th26;

      

       A11: ( Support ( Up ((m *' p),T,i))) = ( Upper_Support ((m *' p),T,i)) by A7, Lm3;

      then

       A12: ( card ( Support ( Up ((m *' p),T,i)))) = i by A7, Def2;

      then

       A13: ( Support ( Up (p,T,i))) = {} implies ( Support ( Up ((m *' p),T,i))) = {} by A4;

       A14:

      now

        assume

         A15: (( term m) + b) in ( Support ( Low ((m *' p),T,i)));

         A16:

        now

          assume (( term m) + b) in ( Support ( Up ((m *' p),T,i)));

          then (( term m) + b) in (( Support ( Up ((m *' p),T,i))) /\ ( Support ( Low ((m *' p),T,i)))) by A15, XBOOLE_0:def 4;

          hence contradiction by A7, A9, A15, Th28;

        end;

        

         A17: ( Support (m *' p)) = { (( term m) + u) where u be Element of ( Bags n) : u in ( Support p) } by Th9;

         A18:

        now

          defpred P[ object, object] means $1 = (( term m) + ( In ($2,( Bags n))));

          assume

           A19: b in ( Support ( Up (p,T,i)));

           A20:

          now

            let b9 be bag of n;

            assume

             A21: (( term m) + b9) in ( Support ( Up ((m *' p),T,i)));

            then

             A22: (( term m) + b) < ((( term m) + b9),T) by A7, A11, A8, A15, Th20;

             not b9 <= (b,T) by A22, TERMORD: 5, Th2;

            then b < (b9,T) by TERMORD: 5;

            then

             A23: b <= (b9,T) by TERMORD:def 3;

            b9 in ( Support p) by A10, A21, Th8;

            hence b9 in ( Support ( Up (p,T,i))) by A1, A3, A19, A23, Def2;

          end;

          

           A24: for x be object st x in ( Support ( Up ((m *' p),T,i))) holds ex y be object st y in ( Support ( Up (p,T,i))) & P[x, y]

          proof

            let x be object;

            assume

             A25: x in ( Support ( Up ((m *' p),T,i)));

            then x in ( Support (m *' p)) by A10;

            then

            consider x9 be Element of ( Bags n) such that

             A26: x = (( term m) + x9) and x9 in ( Support p) by A17;

            take x9;

            thus thesis by A20, A25, A26;

          end;

          consider f be Function of ( Support ( Up ((m *' p),T,i))), ( Support ( Up (p,T,i))) such that

           A27: for x be object st x in ( Support ( Up ((m *' p),T,i))) holds P[x, (f . x)] from FUNCT_2:sch 1( A24);

          now

            let x1,x2 be object;

            assume that

             A28: x1 in ( dom f) and

             A29: x2 in ( dom f) and

             A30: (f . x1) = (f . x2);

            (f . x2) in ( rng f) by A29, FUNCT_1: 3;

            then

             A31: (f . x2) in ( Support ( Up (p,T,i)));

            (f . x1) in ( rng f) by A28, FUNCT_1: 3;

            then (f . x1) in ( Support ( Up (p,T,i)));

            then

            reconsider x19 = (f . x1), x29 = (f . x2) as Element of ( Bags n) by A31;

            

             A32: x19 = ( In (x19,( Bags n)));

            x29 = ( In (x29,( Bags n)));

            

            hence x1 = (( term m) + x19) by A27, A28, A30

            .= x2 by A27, A29, A30, A32;

          end;

          then

           A33: f is one-to-one by FUNCT_1:def 4;

          ( Support ( Up ((m *' p),T,i))) c= ( dom f) by A13, FUNCT_2:def 1;

          then (( Support ( Up ((m *' p),T,i))),(f .: ( Support ( Up ((m *' p),T,i))))) are_equipotent by A33, CARD_1: 33;

          

          then ( card (f .: ( Support ( Up ((m *' p),T,i))))) = ( card ( Support ( Up ((m *' p),T,i)))) by CARD_1: 5

          .= i by A7, A11, Def2;

          then b in (f .: ( Support ( Up ((m *' p),T,i)))) by A4, A19, CARD_2: 102;

          then

          consider bb be object such that

           A34: bb in ( dom f) and

           A35: bb in ( Support ( Up ((m *' p),T,i))) & (f . bb) = b by FUNCT_1:def 6;

          (f . bb) in ( rng f) by A34, FUNCT_1: 3;

          then (f . bb) in ( Support ( Up (p,T,i)));

          then

          reconsider bb9 = (f . bb) as Element of ( Bags n);

          bb9 = ( In (bb9,( Bags n)));

          hence contradiction by A16, A27, A35;

        end;

        (( term m) + b) in ( Support (m *' p)) by A9, A15;

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

        then

        consider u be Element of ( Bags n) such that

         A36: (( term m) + b) = (( term m) + u) and

         A37: u in ( Support p);

        b = ((( term m) + b) -' ( term m)) by PRE_POLY: 48

        .= u by A36, PRE_POLY: 48;

        hence b in ( Support ( Low (p,T,i))) by A1, A37, A18, Th28;

      end;

      

       A38: ( Support ( Up ((m *' p),T,i))) = {} implies ( Support ( Up (p,T,i))) = {} by A12, A4;

      now

        assume

         A39: b in ( Support ( Low (p,T,i)));

         A40:

        now

          assume b in ( Support ( Up (p,T,i)));

          then b in (( Support ( Up (p,T,i))) /\ ( Support ( Low (p,T,i)))) by A39, XBOOLE_0:def 4;

          hence contradiction by A1, A2, A39, Th28;

        end;

         A41:

        now

          defpred P[ object, object] means $2 = (( term m) + ( In ($1,( Bags n))));

          assume

           A42: (( term m) + b) in ( Support ( Up ((m *' p),T,i)));

           A43:

          now

            let b9 be bag of n;

            assume

             A44: b9 in ( Support ( Up (p,T,i)));

            then (( term m) + b) < ((( term m) + b9),T) by A1, A3, A6, A39, Th4, Th20;

            then

             A45: (( term m) + b) <= ((( term m) + b9),T) by TERMORD:def 3;

            (( term m) + b9) in ( Support (m *' p)) by A5, A44, Th8;

            hence (( term m) + b9) in ( Support ( Up ((m *' p),T,i))) by A7, A11, A42, A45, Def2;

          end;

          

           A46: for x be object st x in ( Support ( Up (p,T,i))) holds ex y be object st y in ( Support ( Up ((m *' p),T,i))) & P[x, y]

          proof

            let x be object;

            assume

             A47: x in ( Support ( Up (p,T,i)));

            then

            reconsider x9 = x as Element of ( Bags n);

            take (( term m) + x9);

            thus thesis by A43, A47;

          end;

          consider f be Function of ( Support ( Up (p,T,i))), ( Support ( Up ((m *' p),T,i))) such that

           A48: for x be object st x in ( Support ( Up (p,T,i))) holds P[x, (f . x)] from FUNCT_2:sch 1( A46);

          now

            let x1,x2 be object;

            assume that

             A49: x1 in ( dom f) and

             A50: x2 in ( dom f) and

             A51: (f . x1) = (f . x2);

            x1 in ( Support ( Up (p,T,i))) & x2 in ( Support ( Up (p,T,i))) by A49, A50;

            then

            reconsider x = x1, y = x2 as Element of ( Bags n);

            y = ( In (y,( Bags n)));

            then

             A52: (f . y) = (( term m) + y) by A48, A50;

            x = ( In (x,( Bags n)));

            then

             A53: (f . x) = (( term m) + x) by A48, A49;

            

            thus x1 = ((( term m) + x) -' ( term m)) by PRE_POLY: 48

            .= x2 by A51, A53, A52, PRE_POLY: 48;

          end;

          then

           A54: f is one-to-one by FUNCT_1:def 4;

          ( Support ( Up (p,T,i))) c= ( dom f) by A38, FUNCT_2:def 1;

          then (( Support ( Up (p,T,i))),(f .: ( Support ( Up (p,T,i))))) are_equipotent by A54, CARD_1: 33;

          

          then ( card (f .: ( Support ( Up (p,T,i))))) = ( card ( Support ( Up (p,T,i)))) by CARD_1: 5

          .= i by A1, A3, Def2;

          then (( term m) + b) in (f .: ( Support ( Up (p,T,i)))) by A12, A42, CARD_2: 102;

          then

          consider bb be object such that

           A55: bb in ( dom f) and

           A56: bb in ( Support ( Up (p,T,i))) and

           A57: (f . bb) = (( term m) + b) by FUNCT_1:def 6;

          reconsider bb as Element of ( Bags n) by A56;

          bb = ( In (bb,( Bags n)));

          then

           A58: (( term m) + bb) = (( term m) + b) by A48, A55, A57;

          bb = ((( term m) + bb) -' ( term m)) by PRE_POLY: 48

          .= b by A58, PRE_POLY: 48;

          hence contradiction by A40, A55;

        end;

        (( term m) + b) in ( Support (m *' p)) by A2, A39, Th8;

        hence (( term m) + b) in ( Support ( Low ((m *' p),T,i))) by A7, A41, Th28;

      end;

      hence thesis by A14;

    end;

    theorem :: GROEB_3:41

    

     Th41: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i < ( card ( Support p)) holds ( Support ( Low (p,T,(i + 1)))) c= ( Support ( Low (p,T,i)))

    proof

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

      set l = ( Low (p,T,i)), l1 = ( Low (p,T,(i + 1)));

      assume

       A1: i < ( card ( Support p));

      then

       A2: (i + 1) <= ( card ( Support p)) by NAT_1: 13;

      then

       A3: (( card ( Support p)) - i) >= 1 by XREAL_1: 19;

      

       A4: ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by A1, Lm3;

      then ( card ( Support l)) = (( card ( Support p)) - i) by A1, Th24;

      then

       A5: ( HT (( Low (p,T,i)),T)) in ( Lower_Support (p,T,i)) by A3, A4, CARD_1: 27, TERMORD:def 6;

      

       A6: ( HT (( Low (p,T,(i + 1))),T)) <= (( HT (( Low (p,T,i)),T)),T) by A1, Th38;

      

       A7: ( Support ( Low (p,T,(i + 1)))) c= ( Support p) by A2, Th26;

      let u9 be object;

      assume

       A8: u9 in ( Support l1);

      then

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

      u <= (( HT (( Low (p,T,(i + 1))),T)),T) by A8, TERMORD:def 6;

      hence u9 in ( Support l) by A1, A7, A4, A6, A5, A8, Th24, TERMORD: 8;

    end;

    theorem :: GROEB_3:42

    

     Th42: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of n, L, i be Element of NAT st i < ( card ( Support p)) holds (( Support ( Low (p,T,i))) \ ( Support ( Low (p,T,(i + 1))))) = {( HT (( Low (p,T,i)),T))}

    proof

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

      set l = ( Low (p,T,i)), l1 = ( Low (p,T,(i + 1)));

      assume

       A1: i < ( card ( Support p));

      then

       A2: ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by Lm3;

      then

       A3: ( card ( Support l)) = (( card ( Support p)) - i) by A1, Th24;

      now

        assume ( Lower_Support (p,T,i)) = {} ;

        then (( card ( Support p)) - i) = 0 by A1, Th24, CARD_1: 27;

        hence contradiction by A1;

      end;

      then

       A4: ( HT (( Low (p,T,i)),T)) in ( Support l) by A2, TERMORD:def 6;

      

       A5: ( Support ( Low (p,T,i))) c= ( Support p) by A1, Th26;

      

       A6: (i + 1) <= ( card ( Support p)) by A1, NAT_1: 13;

      then ( Support ( Low (p,T,(i + 1)))) = ( Lower_Support (p,T,(i + 1))) by Lm3;

      then

       A7: ( card ( Support l1)) = (( card ( Support p)) - (i + 1)) by A6, Th24;

      

      then ( card (( Support ( Low (p,T,i))) \ ( Support ( Low (p,T,(i + 1)))))) = ((( card ( Support p)) - i) - (( card ( Support p)) - (i + 1))) by A1, A3, Th41, CARD_2: 44

      .= 1;

      then

      consider x be object such that

       A8: (( Support ( Low (p,T,i))) \ ( Support ( Low (p,T,(i + 1))))) = {x} by CARD_2: 42;

      

       A9: ( Support ( Low (p,T,(i + 1)))) = ( Lower_Support (p,T,(i + 1))) by A6, Lm3;

      now

        assume

         A10: x <> ( HT (( Low (p,T,i)),T));

         A11:

        now

          assume not ( HT (( Low (p,T,i)),T)) in ( Support l1);

          then ( HT (( Low (p,T,i)),T)) in (( Support l) \ ( Support l1)) by A4, XBOOLE_0:def 5;

          hence contradiction by A8, A10, TARSKI:def 1;

        end;

         A12:

        now

          let u be object;

          assume

           A13: u in ( Support l);

          then

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

          u9 <= (( HT (( Low (p,T,i)),T)),T) by A13, TERMORD:def 6;

          hence u in ( Support l1) by A6, A5, A9, A11, A13, Th24;

        end;

        ( Support ( Low (p,T,(i + 1)))) c= ( Support ( Low (p,T,i))) by A1, Th41;

        then for u be object holds u in ( Support l1) implies u in ( Support l);

        then (( card ( Support p)) + ( - i)) <= (( card ( Support p)) + ( - (i + 1))) by A3, A7, A12, TARSKI: 2;

        then ( - i) <= ( - (i + 1)) by XREAL_1: 6;

        then (i + 1) <= i by XREAL_1: 24;

        then ((i + 1) - i) <= (i - i) by XREAL_1: 9;

        then 1 <= 0 ;

        hence contradiction;

      end;

      hence thesis by A8;

    end;

    theorem :: GROEB_3:43

    

     Th43: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_zeroed right_complementable non trivial addLoopStr, p be Polynomial of n, L, i be Element of NAT st i < ( card ( Support p)) holds ( Low (p,T,(i + 1))) = ( Red (( Low (p,T,i)),T))

    proof

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

      set l = ( Low (p,T,i)), l1 = ( Low (p,T,(i + 1))), r = ( Red (l,T));

      assume

       A1: i < ( card ( Support p));

      then

       A2: ( Support ( Low (p,T,i))) c= ( Support p) by Th26;

      ( Support ( Low (p,T,i))) = ( Lower_Support (p,T,i)) by A1, Lm3;

      then

       A3: ( card ( Support l)) = (( card ( Support p)) - i) by A1, Th24;

      

       A4: ( Support ( Low (p,T,(i + 1)))) c= ( Support ( Low (p,T,i))) by A1, Th41;

      

       A5: (i + 1) <= ( card ( Support p)) by A1, NAT_1: 13;

      then ( Support ( Low (p,T,(i + 1)))) = ( Lower_Support (p,T,(i + 1))) by Lm3;

      then

       A6: ( card ( Support l1)) = (( card ( Support p)) - (i + 1)) by A5, Th24;

      

       A7: ( Support ( Low (p,T,(i + 1)))) = ( Lower_Support (p,T,(i + 1))) by A5, Lm3;

      now

        set u = the Element of ( {( HT (l,T))} /\ ( Support l1));

        assume

         A8: ( {( HT (l,T))} /\ ( Support l1)) <> {} ;

        then u in {( HT (l,T))} by XBOOLE_0:def 4;

        then

         A9: u = ( HT (l,T)) by TARSKI:def 1;

        

         A10: u in ( Support l1) by A8, XBOOLE_0:def 4;

        now

          let u9 be object;

          assume

           A11: u9 in ( Support l);

          then

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

          u <= (( HT (( Low (p,T,i)),T)),T) by A11, TERMORD:def 6;

          hence u9 in ( Support l1) by A5, A2, A7, A10, A9, A11, Th24;

        end;

        then ( Support l) c= ( Support l1);

        then (( card ( Support p)) + ( - i)) <= (( card ( Support p)) + ( - (i + 1))) by A3, A6, NAT_1: 43;

        then ( - i) <= ( - (i + 1)) by XREAL_1: 6;

        then (i + 1) <= i by XREAL_1: 24;

        then ((i + 1) - i) <= (i - i) by XREAL_1: 9;

        then 1 <= 0 ;

        hence contradiction;

      end;

      then

       A12: ( Support l1) misses {( HT (l,T))} by XBOOLE_0:def 7;

      

       A13: (( Support ( Low (p,T,i))) \ ( Support ( Low (p,T,(i + 1))))) = {( HT (( Low (p,T,i)),T))} by A1, Th42;

      then ( Support ( Low (p,T,i))) = (( Support l1) \/ {( HT (l,T))}) by A1, Th41, XBOOLE_1: 45;

      

      then

       A14: ( Support r) = ((( Support l1) \/ {( HT (l,T))}) \ {( HT (l,T))}) by TERMORD: 36

      .= (( Support l1) \ {( HT (l,T))}) by XBOOLE_1: 40

      .= ( Support l1) by A12, XBOOLE_1: 83;

       A15:

      now

        let x be object;

        assume x in ( dom l1);

        then

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

        now

          per cases ;

            case

             A16: b in ( Support l1);

            then not b in {( HT (( Low (p,T,i)),T))} by A13, XBOOLE_0:def 5;

            then

             A17: b <> ( HT (l,T)) by TARSKI:def 1;

            

            thus (l1 . b) = (p . b) by A5, A16, Th31

            .= (l . b) by A1, A4, A16, Th31

            .= (r . b) by A4, A16, A17, TERMORD: 40;

          end;

            case

             A18: not b in ( Support l1);

            

            hence (l1 . b) = ( 0. L) by POLYNOM1:def 4

            .= (r . b) by A14, A18, POLYNOM1:def 4;

          end;

        end;

        hence (l1 . x) = (r . x);

      end;

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

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

      hence thesis by A15, FUNCT_1: 2;

    end;

    theorem :: GROEB_3:44

    

     Th44: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive domRing-like non trivial doubleLoopStr, p be Polynomial of n, L, m be non-zero Monomial of n, L, i be Element of NAT st i <= ( card ( Support p)) holds ( Low ((m *' p),T,i)) = (m *' ( Low (p,T,i)))

    proof

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

      set l = ( Low (p,T,i)), lm = ( Low ((m *' p),T,i));

      assume

       A1: i <= ( card ( Support p));

      then

       A2: i <= ( card ( Support (m *' p))) by Th10;

      

       A3: ( Support (m *' l)) c= { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support l) } by TERMORD: 30;

       A4:

      now

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

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

        then

         A5: ( Support m) = {( term m)} by POLYNOM7: 7;

        then ( term m) in ( Support m) by TARSKI:def 1;

        then

         A6: (m . ( term m)) <> ( 0. L) by POLYNOM1:def 4;

        let u be object;

        assume

         A7: u in ( Support (m *' l));

        then

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

        u in { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support l) } by A3, A7;

        then

        consider s,t be Element of ( Bags n) such that

         A8: u9 = (s + t) and

         A9: s in ( Support m) and

         A10: t in ( Support l);

        

         A11: (l . t) <> ( 0. L) by A10, POLYNOM1:def 4;

        

         A12: ( term m) = s by A9, A5, TARSKI:def 1;

        

        then ((m *' p) . u9) = ((m . ( term m)) * (p . t)) by A8, POLYRED: 7

        .= ((m . ( term m)) * (l . t)) by A1, A10, Th31;

        then ((m *' p) . u9) <> ( 0. L) by A11, A6, VECTSP_2:def 1;

        then

         A13: u9 in ( Support (m *' p)) by POLYNOM1:def 4;

        now

          assume not (s + t) in ( Support ( Low ((m *' p),T,i)));

          then

           A14: (s + t) in ( Support ( Up ((m *' p),T,i))) by A2, A8, A13, Th28;

          now

            let t9 be bag of n;

            assume t9 in ( Support ( Low (p,T,i)));

            then (s + t9) in ( Support ( Low ((m *' p),T,i))) by A1, A12, Th40;

            then

             A15: (s + t9) < ((s + t),T) by A2, A14, Th29;

             not t <= (t9,T) by A15, TERMORD: 5, Th2;

            hence t9 < (t,T) by TERMORD: 5;

          end;

          then t < (t,T) by A10;

          hence contradiction by TERMORD:def 3;

        end;

        hence u in ( Support lm) by A8;

      end;

      

       A16: ( Support (m *' p)) c= { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support p) } by TERMORD: 30;

      now

        let u be object;

        assume

         A17: u in ( Support ( Low ((m *' p),T,i)));

        then

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

        ( Support ( Low ((m *' p),T,i))) c= ( Support (m *' p)) by A2, Th26;

        then u9 in ( Support (m *' p)) by A17;

        then

         A18: u9 in { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support p) } by A16;

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

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

        then

         A19: ( Support m) = {( term m)} by POLYNOM7: 7;

        then ( term m) in ( Support m) by TARSKI:def 1;

        then

         A20: (m . ( term m)) <> ( 0. L) by POLYNOM1:def 4;

        consider s,t be Element of ( Bags n) such that

         A21: u = (s + t) and

         A22: s in ( Support m) and

         A23: t in ( Support p) by A18;

        

         A24: (p . t) <> ( 0. L) by A23, POLYNOM1:def 4;

        

         A25: ( term m) = s by A22, A19, TARSKI:def 1;

        then

         A26: t in ( Support l) by A1, A17, A21, Th40;

        ((m *' l) . (( term m) + t)) = ((m . ( term m)) * (l . t)) by POLYRED: 7

        .= ((m . ( term m)) * (p . t)) by A1, A26, Th31;

        then ((m *' l) . u9) <> ( 0. L) by A21, A20, A25, A24, VECTSP_2:def 1;

        hence u in ( Support (m *' ( Low (p,T,i)))) by POLYNOM1:def 4;

      end;

      then

       A27: ( Support (m *' l)) = ( Support lm) by A4, TARSKI: 2;

       A28:

      now

        let x be object;

        assume x in ( dom (m *' l));

        then

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

        now

          per cases ;

            case

             A29: b in ( Support (m *' l));

            then

             A30: b in { (s + t) where s,t be Element of ( Bags n) : s in ( Support m) & t in ( Support l) } by A3;

            

             A31: b in ( Support lm) by A4, A29;

            consider s,t be Element of ( Bags n) such that

             A32: b = (s + t) and

             A33: s in ( Support m) and

             A34: t in ( Support l) by A30;

            ( Support m) = {( term m)} by A33, POLYNOM7: 7;

            then

             A35: ( term m) = s by A33, TARSKI:def 1;

            

            hence ((m *' l) . b) = ((m . ( term m)) * (l . t)) by A32, POLYRED: 7

            .= ((m . ( term m)) * (p . t)) by A1, A34, Th31

            .= ((m *' p) . b) by A32, A35, POLYRED: 7

            .= (lm . b) by A2, A31, Th31;

          end;

            case

             A36: not b in ( Support (m *' l));

            

            hence ((m *' l) . b) = ( 0. L) by POLYNOM1:def 4

            .= (lm . b) by A27, A36, POLYNOM1:def 4;

          end;

        end;

        hence ((m *' l) . x) = (lm . x);

      end;

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

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

      hence thesis by A28, FUNCT_1: 2;

    end;

    begin

    

     Lm4: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), R be RedSequence of ( PolyRedRel (P,T)), i be Element of NAT st 1 <= i & i <= ( len R) & ( len R) > 1 holds (R . i) is Polynomial of n, L

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), R be RedSequence of ( PolyRedRel (P,T)), i be Element of NAT ;

      assume that

       A1: 1 <= i and

       A2: i <= ( len R) and

       A3: 1 < ( len R);

      

       A4: i in ( dom R) by A1, A2, FINSEQ_3: 25;

      now

        per cases ;

          case i <> ( len R);

          then i < ( len R) by A2, XXREAL_0: 1;

          then 1 <= (i + 1) & (i + 1) <= ( len R) by NAT_1: 11, NAT_1: 13;

          then (i + 1) in ( dom R) by FINSEQ_3: 25;

          then [(R . i), (R . (i + 1))] in ( PolyRedRel (P,T)) by A4, REWRITE1:def 2;

          then (R . i) in ( dom ( PolyRedRel (P,T))) by XTUPLE_0:def 12;

          then (R . i) in the carrier of ( Polynom-Ring (n,L)) by XBOOLE_0:def 5;

          hence thesis by POLYNOM1:def 11;

        end;

          case

           A5: i = ( len R);

          

           A6: (i - 1) is Element of NAT by A1, INT_1: 5;

          (1 + ( - 1)) < (i + ( - 1)) by A3, A5, XREAL_1: 8;

          then

           A7: 1 <= (i - 1) by A6, NAT_1: 14;

          

           A8: i = ((i - 1) + 1);

          (i - 1) <= ( len R) by A5, XREAL_1: 146;

          then (i - 1) in ( dom R) by A6, A7, FINSEQ_3: 25;

          then [(R . (i - 1)), (R . i)] in ( PolyRedRel (P,T)) by A4, A8, REWRITE1:def 2;

          then (R . i) in ( rng ( PolyRedRel (P,T))) by XTUPLE_0:def 13;

          hence thesis by POLYNOM1:def 11;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:45

    

     Th45: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g,p be Polynomial of n, L st f reduces_to (g,p,T) holds ( - f) reduces_to (( - g),p,T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g,p be Polynomial of n, L;

      assume f reduces_to (g,p,T);

      then

      consider b be bag of n such that

       A1: f reduces_to (g,p,b,T) by POLYRED:def 6;

      b in ( Support f) by A1, POLYRED:def 5;

      then

       A2: b in ( Support ( - f)) by GROEB_1: 5;

      consider s be bag of n such that

       A3: (s + ( HT (p,T))) = b and

       A4: g = (f - (((f . b) / ( HC (p,T))) * (s *' p))) by A1, POLYRED:def 5;

      g = (f + ( - (((f . b) / ( HC (p,T))) * (s *' p)))) by A4, POLYNOM1:def 7;

      

      then

       A5: ( - g) = (( - f) + ( - ( - (((f . b) / ( HC (p,T))) * (s *' p))))) by POLYRED: 1

      .= (( - f) - ( - (((f . b) / ( HC (p,T))) * (s *' p)))) by POLYNOM1:def 7

      .= (( - f) - (( - ((f . b) / ( HC (p,T)))) * (s *' p))) by POLYRED: 9

      .= (( - f) - (( - ((f . b) * (( HC (p,T)) " ))) * (s *' p)))

      .= (( - f) - ((( - (f . b)) * (( HC (p,T)) " )) * (s *' p))) by VECTSP_1: 9

      .= (( - f) - ((( - (f . b)) / ( HC (p,T))) * (s *' p)))

      .= (( - f) - (((( - f) . b) / ( HC (p,T))) * (s *' p))) by POLYNOM1: 17;

       A6:

      now

        

         A7: ( - ( - f)) = f by POLYNOM1: 19;

        assume ( - f) = ( 0_ (n,L));

        

        then f = ( - ( 0_ (n,L))) by A7

        .= ( 0_ (n,L)) by Th13;

        hence contradiction by A1, POLYRED:def 5;

      end;

      p <> ( 0_ (n,L)) by A1, POLYRED:def 5;

      then ( - f) reduces_to (( - g),p,b,T) by A3, A6, A5, A2, POLYRED:def 5;

      hence thesis by POLYRED:def 6;

    end;

    

     Lm5: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L st (( HT (p1,T)),( HT (p2,T))) are_disjoint holds for b1,b2 be bag of n st b1 in ( Support p1) & b2 in ( Support p2) holds not (b1 = ( HT (p1,T)) & b2 = ( HT (p2,T))) implies not ((( HT (p1,T)) + b2) = (( HT (p2,T)) + b1))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L;

      assume

       A1: (( HT (p1,T)),( HT (p2,T))) are_disjoint ;

      let b1,b2 be bag of n;

      assume that

       A2: b1 in ( Support p1) and

       A3: b2 in ( Support p2);

      assume

       A4: not (b1 = ( HT (p1,T)) & b2 = ( HT (p2,T)));

      b2 <= (( HT (p2,T)),T) by A3, TERMORD:def 6;

      then

       A5: (( HT (p1,T)) + b2) <= ((( HT (p1,T)) + ( HT (p2,T))),T) by Th2;

      b1 <= (( HT (p1,T)),T) by A2, TERMORD:def 6;

      then

       A6: (( HT (p2,T)) + b1) <= ((( HT (p1,T)) + ( HT (p2,T))),T) by Th2;

      assume

       A7: (( HT (p1,T)) + b2) = (( HT (p2,T)) + b1);

      then

       A8: ( HT (p1,T)) divides (( HT (p2,T)) + b1) by PRE_POLY: 50;

      

       A9: ( HT (p2,T)) divides (( HT (p1,T)) + b2) by A7, PRE_POLY: 50;

      now

        per cases by A4;

          case

           A10: not b1 = ( HT (p1,T));

          ( HT (p2,T)) divides (( HT (p2,T)) + b1) by PRE_POLY: 50;

          then ( lcm (( HT (p1,T)),( HT (p2,T)))) divides (( HT (p2,T)) + b1) by A8, GROEB_2: 4;

          then (( HT (p1,T)) + ( HT (p2,T))) divides (( HT (p2,T)) + b1) by A1, GROEB_2: 5;

          then (( HT (p1,T)) + ( HT (p2,T))) <= ((( HT (p2,T)) + b1),T) by TERMORD: 10;

          then

           A11: (( HT (p1,T)) + ( HT (p2,T))) = (( HT (p2,T)) + b1) by A6, TERMORD: 7;

          ( HT (p1,T)) = ((( HT (p1,T)) + ( HT (p2,T))) -' ( HT (p2,T))) by PRE_POLY: 48;

          hence contradiction by A10, A11, PRE_POLY: 48;

        end;

          case

           A12: not b2 = ( HT (p2,T));

          ( HT (p1,T)) divides (( HT (p1,T)) + b2) by PRE_POLY: 50;

          then ( lcm (( HT (p1,T)),( HT (p2,T)))) divides (( HT (p1,T)) + b2) by A9, GROEB_2: 4;

          then (( HT (p1,T)) + ( HT (p2,T))) divides (( HT (p1,T)) + b2) by A1, GROEB_2: 5;

          then (( HT (p1,T)) + ( HT (p2,T))) <= ((( HT (p1,T)) + b2),T) by TERMORD: 10;

          then

           A13: (( HT (p1,T)) + ( HT (p2,T))) = (( HT (p1,T)) + b2) by A5, TERMORD: 7;

          ( HT (p2,T)) = ((( HT (p1,T)) + ( HT (p2,T))) -' ( HT (p1,T))) by PRE_POLY: 48;

          hence contradiction by A12, A13, PRE_POLY: 48;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:46

    

     Th46: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,f1,g,p be Polynomial of n, L st f reduces_to (f1, {p},T) & for b1 be bag of n st b1 in ( Support g) holds not (( HT (p,T)) divides b1) holds (f + g) reduces_to ((f1 + g), {p},T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,f1,g,p be Polynomial of n, L;

      assume that

       A1: f reduces_to (f1, {p},T) and

       A2: for b1 be bag of n st b1 in ( Support g) holds not ( HT (p,T)) divides b1;

      consider q be Polynomial of n, L such that

       A3: q in {p} and

       A4: f reduces_to (f1,q,T) by A1, POLYRED:def 7;

      p = q by A3, TARSKI:def 1;

      then

      consider br be bag of n such that

       A5: f reduces_to (f1,p,br,T) by A4, POLYRED:def 6;

      consider s be bag of n such that

       A6: (s + ( HT (p,T))) = br and

       A7: f1 = (f - (((f . br) / ( HC (p,T))) * (s *' p))) by A5, POLYRED:def 5;

      

       A8: not br in ( Support g) by A6, TERMORD: 1, A2;

      

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

      

       A10: p in {p} by TARSKI:def 1;

      

       A11: br in ( Support f) by A5, POLYRED:def 5;

      

       A12: ((f + g) . br) = ((f . br) + (g . br)) by POLYNOM1: 15

      .= ((f . br) + ( 0. L)) by A8, A9, POLYNOM1:def 4

      .= (f . br) by RLVECT_1:def 4;

      

       A13: p <> ( 0_ (n,L)) by A5, POLYRED:def 5;

      now

        per cases ;

          case (f + g) = ( 0_ (n,L));

          then ((f + g) - f) = ( - f) by Th14;

          then ((f + g) + ( - f)) = ( - f) by POLYNOM1:def 7;

          then ((f + ( - f)) + g) = ( - f) by POLYNOM1: 21;

          then (( 0_ (n,L)) + g) = ( - f) by POLYRED: 3;

          then g = ( - f) by POLYRED: 2;

          hence contradiction by A11, A8, GROEB_1: 5;

        end;

          case

           A14: (f + g) <> ( 0_ (n,L));

          set g1 = ((f + g) - ((((f + g) . br) / ( HC (p,T))) * (s *' p)));

          ((f + g) . br) <> ( 0. L) by A11, A12, POLYNOM1:def 4;

          then br in ( Support (f + g)) by A11, POLYNOM1:def 4;

          then (f + g) reduces_to (g1,p,br,T) by A13, A6, A14, POLYRED:def 5;

          then

           A15: (f + g) reduces_to (g1,p,T) by POLYRED:def 6;

          g1 = ((f + g) + ( - (((f . br) / ( HC (p,T))) * (s *' p)))) by A12, POLYNOM1:def 7

          .= ((f + ( - (((f . br) / ( HC (p,T))) * (s *' p)))) + g) by POLYNOM1: 21

          .= (f1 + g) by A7, POLYNOM1:def 7;

          hence thesis by A10, A15, POLYRED:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:47

    

     Th47: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g be non-zero Polynomial of n, L holds (f *' g) reduces_to ((( Red (f,T)) *' g), {g},T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g be non-zero Polynomial of n, L;

      set fg = (f *' g);

      set q = (fg - (((fg . ( HT (fg,T))) / ( HC (g,T))) * (( HT (f,T)) *' g)));

      reconsider r = ( - ( HM (f,T))) as Polynomial of n, L;

      

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

      

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

      

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

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

      then

       A4: ( HT (fg,T)) in ( Support fg) by TERMORD:def 6;

      ( HT (fg,T)) = (( HT (f,T)) + ( HT (g,T))) by TERMORD: 31;

      then fg reduces_to (q,g,( HT (fg,T)),T) by A3, A1, A4, POLYRED:def 5;

      then

       A5: g in {g} & fg reduces_to (q,g,T) by POLYRED:def 6, TARSKI:def 1;

      q = (fg - ((( HC (fg,T)) / ( HC (g,T))) * (( HT (f,T)) *' g))) by TERMORD:def 7

      .= (fg - (((( HC (f,T)) * ( HC (g,T))) / ( HC (g,T))) * (( HT (f,T)) *' g))) by TERMORD: 32

      .= (fg - (((( HC (f,T)) * ( HC (g,T))) * (( HC (g,T)) " )) * (( HT (f,T)) *' g)))

      .= (fg - ((( HC (f,T)) * (( HC (g,T)) * (( HC (g,T)) " ))) * (( HT (f,T)) *' g))) by GROUP_1:def 3

      .= (fg - ((( HC (f,T)) * ( 1. L)) * (( HT (f,T)) *' g))) by A2, VECTSP_1:def 10

      .= (fg - (( HC (f,T)) * (( HT (f,T)) *' g)))

      .= (fg - (( Monom (( HC (f,T)),( HT (f,T)))) *' g)) by POLYRED: 22

      .= (fg - (( HM (f,T)) *' g)) by TERMORD:def 8

      .= (fg + ( - (( HM (f,T)) *' g))) by POLYNOM1:def 7

      .= (fg + (r *' g)) by POLYRED: 6

      .= (g *' (f + ( - ( HM (f,T))))) by POLYNOM1: 26

      .= ((f - ( HM (f,T))) *' g) by POLYNOM1:def 7

      .= (( Red (f,T)) *' g) by TERMORD:def 9;

      hence thesis by A5, POLYRED:def 7;

    end;

    theorem :: GROEB_3:48

    for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g be non-zero Polynomial of n, L, p be Polynomial of n, L st (p . ( HT ((f *' g),T))) = ( 0. L) holds ((f *' g) + p) reduces_to (((( Red (f,T)) *' g) + p), {g},T)

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g be non-zero Polynomial of n, L, p be Polynomial of n, L;

      assume

       A1: (p . ( HT ((f *' g),T))) = ( 0. L);

      (f *' g) <> ( 0_ (n,L)) by POLYNOM7:def 1;

      then ( Support (f *' g)) <> {} by POLYNOM7: 1;

      then ( HT ((f *' g),T)) in ( Support (f *' g)) by TERMORD:def 6;

      then

       A2: ((f *' g) . ( HT ((f *' g),T))) <> ( 0. L) by POLYNOM1:def 4;

      reconsider r = ( - ( HM (f,T))) as Polynomial of n, L;

      set fg = ((f *' g) + p);

      set q = (fg - (((fg . ( HT ((f *' g),T))) / ( HC (g,T))) * (( HT (f,T)) *' g)));

      

       A3: ( HT ((f *' g),T)) = (( HT (f,T)) + ( HT (g,T))) by TERMORD: 31;

      

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

      

       A5: ( HC (g,T)) <> ( 0. L);

      (fg . ( HT ((f *' g),T))) = (((f *' g) . ( HT ((f *' g),T))) + (p . ( HT ((f *' g),T)))) by POLYNOM1: 15

      .= ((f *' g) . ( HT ((f *' g),T))) by A1, RLVECT_1:def 4;

      then

       A6: ( HT ((f *' g),T)) in ( Support fg) by A2, POLYNOM1:def 4;

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

      then fg reduces_to (q,g,( HT ((f *' g),T)),T) by A6, A4, A3, POLYRED:def 5;

      then

       A7: g in {g} & fg reduces_to (q,g,T) by POLYRED:def 6, TARSKI:def 1;

      q = (fg - (((((f *' g) . ( HT ((f *' g),T))) + ( 0. L)) / ( HC (g,T))) * (( HT (f,T)) *' g))) by A1, POLYNOM1: 15

      .= (fg - ((((f *' g) . ( HT ((f *' g),T))) / ( HC (g,T))) * (( HT (f,T)) *' g))) by RLVECT_1:def 4

      .= (fg - ((( HC ((f *' g),T)) / ( HC (g,T))) * (( HT (f,T)) *' g))) by TERMORD:def 7

      .= (fg - (((( HC (f,T)) * ( HC (g,T))) / ( HC (g,T))) * (( HT (f,T)) *' g))) by TERMORD: 32

      .= (fg - (((( HC (f,T)) * ( HC (g,T))) * (( HC (g,T)) " )) * (( HT (f,T)) *' g)))

      .= (fg - ((( HC (f,T)) * (( HC (g,T)) * (( HC (g,T)) " ))) * (( HT (f,T)) *' g))) by GROUP_1:def 3

      .= (fg - ((( HC (f,T)) * ( 1. L)) * (( HT (f,T)) *' g))) by A5, VECTSP_1:def 10

      .= (fg - (( HC (f,T)) * (( HT (f,T)) *' g)))

      .= (fg - (( Monom (( HC (f,T)),( HT (f,T)))) *' g)) by POLYRED: 22

      .= (fg - (( HM (f,T)) *' g)) by TERMORD:def 8

      .= (fg + ( - (( HM (f,T)) *' g))) by POLYNOM1:def 7

      .= (((f *' g) + p) + (r *' g)) by POLYRED: 6

      .= (((f *' g) + (r *' g)) + p) by POLYNOM1: 21

      .= ((g *' (f + ( - ( HM (f,T))))) + p) by POLYNOM1: 26

      .= (((f - ( HM (f,T))) *' g) + p) by POLYNOM1:def 7

      .= ((( Red (f,T)) *' g) + p) by TERMORD:def 9;

      hence thesis by A7, POLYRED:def 7;

    end;

    theorem :: GROEB_3:49

    

     Th49: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L st ( PolyRedRel (P,T)) reduces (f,g) holds ( PolyRedRel (P,T)) reduces (( - f),( - g))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), f,g be Polynomial of n, L;

      assume ( PolyRedRel (P,T)) reduces (f,g);

      then

      consider R be RedSequence of ( PolyRedRel (P,T)) such that

       A1: (R . 1) = f and

       A2: (R . ( len R)) = g by REWRITE1:def 3;

      defpred P[ Nat] means for q be Polynomial of n, L st q = (R . $1) holds ( PolyRedRel (P,T)) reduces (( - f),( - q));

      

       A3: 1 <= ( len R) by NAT_1: 14;

       A4:

      now

        let k be Element of NAT ;

        assume

         A5: 1 <= k & k < ( len R);

        then 1 < ( len R) by XXREAL_0: 2;

        then

        reconsider p = (R . k) as Polynomial of n, L by A5, Lm4;

        assume P[k];

        then

         A6: ( PolyRedRel (P,T)) reduces (( - f),( - p));

        now

          let q be Polynomial of n, L;

          assume

           A7: q = (R . (k + 1));

          1 <= (k + 1) & (k + 1) <= ( len R) by A5, NAT_1: 13;

          then

           A8: (k + 1) in ( dom R) by FINSEQ_3: 25;

          k in ( dom R) by A5, FINSEQ_3: 25;

          then [(R . k), (R . (k + 1))] in ( PolyRedRel (P,T)) by A8, REWRITE1:def 2;

          then p reduces_to (q,P,T) by A7, POLYRED:def 13;

          then

          consider l be Polynomial of n, L such that

           A9: l in P and

           A10: p reduces_to (q,l,T) by POLYRED:def 7;

          ( - p) reduces_to (( - q),l,T) by A10, Th45;

          then ( - p) reduces_to (( - q),P,T) by A9, POLYRED:def 7;

          then [( - p), ( - q)] in ( PolyRedRel (P,T)) by POLYRED:def 13;

          then ( PolyRedRel (P,T)) reduces (( - p),( - q)) by REWRITE1: 15;

          hence ( PolyRedRel (P,T)) reduces (( - f),( - q)) by A6, REWRITE1: 16;

        end;

        hence P[(k + 1)];

      end;

      

       A11: P[1] by A1, REWRITE1: 12;

      for i be Element of NAT st 1 <= i & i <= ( len R) holds P[i] from INT_1:sch 7( A11, A4);

      hence thesis by A2, A3;

    end;

    theorem :: GROEB_3:50

    for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,f1,g,p be Polynomial of n, L st ( PolyRedRel ( {p},T)) reduces (f,f1) & for b1 be bag of n st b1 in ( Support g) holds not (( HT (p,T)) divides b1) holds ( PolyRedRel ( {p},T)) reduces ((f + g),(f1 + g))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,f1,g,p be Polynomial of n, L;

      assume that

       A1: ( PolyRedRel ( {p},T)) reduces (f,f1) and

       A2: for b1 be bag of n st b1 in ( Support g) holds not ( HT (p,T)) divides b1;

      consider R be RedSequence of ( PolyRedRel ( {p},T)) such that

       A3: (R . 1) = f and

       A4: (R . ( len R)) = f1 by A1, REWRITE1:def 3;

      defpred P[ Nat] means for q be Polynomial of n, L st q = (R . $1) holds ( PolyRedRel ( {p},T)) reduces ((f + g),(q + g));

       A5:

      now

        let k be Element of NAT ;

        assume

         A6: 1 <= k & k < ( len R);

        then 1 < ( len R) by XXREAL_0: 2;

        then

        reconsider h = (R . k) as Polynomial of n, L by A6, Lm4;

        assume P[k];

        then

         A7: ( PolyRedRel ( {p},T)) reduces ((f + g),(h + g));

        now

          let q be Polynomial of n, L;

          assume

           A8: q = (R . (k + 1));

          1 <= (k + 1) & (k + 1) <= ( len R) by A6, NAT_1: 13;

          then

           A9: (k + 1) in ( dom R) by FINSEQ_3: 25;

          k in ( dom R) by A6, FINSEQ_3: 25;

          then [(R . k), (R . (k + 1))] in ( PolyRedRel ( {p},T)) by A9, REWRITE1:def 2;

          then h reduces_to (q, {p},T) by A8, POLYRED:def 13;

          then (h + g) reduces_to ((q + g), {p},T) by A2, Th46;

          then [(h + g), (q + g)] in ( PolyRedRel ( {p},T)) by POLYRED:def 13;

          then ( PolyRedRel ( {p},T)) reduces ((h + g),(q + g)) by REWRITE1: 15;

          hence ( PolyRedRel ( {p},T)) reduces ((f + g),(q + g)) by A7, REWRITE1: 16;

        end;

        hence P[(k + 1)];

      end;

      

       A10: 1 <= ( len R) by NAT_1: 14;

      

       A11: P[1] by A3, REWRITE1: 12;

      for i be Element of NAT st 1 <= i & i <= ( len R) holds P[i] from INT_1:sch 7( A11, A5);

      hence thesis by A4, A10;

    end;

    theorem :: GROEB_3:51

    

     Th51: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g be non-zero Polynomial of n, L holds ( PolyRedRel ( {g},T)) reduces ((f *' g),( 0_ (n,L)))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, f,g be non-zero Polynomial of n, L;

      defpred P[ Nat] means for f be Polynomial of n, L st ( card ( Support f)) = $1 holds ( PolyRedRel ( {g},T)) reduces ((f *' g),( 0_ (n,L)));

      

       A1: ex n be Element of NAT st ( card ( Support f)) = n;

       A2:

      now

        let k be Nat;

        assume

         A3: P[k];

        now

          let f be Polynomial of n, L;

          set rf = ( Red (f,T));

          assume

           A4: ( card ( Support f)) = (k + 1);

          now

            assume f = ( 0_ (n,L));

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

            hence contradiction by A4;

          end;

          then

          reconsider f1 = f as non-zero Polynomial of n, L by POLYNOM7:def 1;

          (f1 *' g) reduces_to ((rf *' g), {g},T) by Th47;

          then [(f1 *' g), (rf *' g)] in ( PolyRedRel ( {g},T)) by POLYRED:def 13;

          then

           A5: ( PolyRedRel ( {g},T)) reduces ((f *' g),(rf *' g)) by REWRITE1: 15;

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

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

          then ( HT (f,T)) in ( Support f) by TERMORD:def 6;

          then for u be object st u in {( HT (f,T))} holds u in ( Support f) by TARSKI:def 1;

          then

           A6: {( HT (f,T))} c= ( Support f);

          ( Support rf) = (( Support f) \ {( HT (f,T))}) by TERMORD: 36;

          

          then ( card ( Support rf)) = (( card ( Support f)) - ( card {( HT (f,T))})) by A6, CARD_2: 44

          .= ((k + 1) - 1) by A4, CARD_1: 30

          .= (k + 0 );

          then ( PolyRedRel ( {g},T)) reduces ((rf *' g),( 0_ (n,L))) by A3;

          hence ( PolyRedRel ( {g},T)) reduces ((f *' g),( 0_ (n,L))) by A5, REWRITE1: 16;

        end;

        hence P[(k + 1)];

      end;

      now

        let f be Polynomial of n, L;

        assume ( card ( Support f)) = 0 ;

        then ( Support f) = {} ;

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

        then (f *' g) = ( 0_ (n,L)) by POLYRED: 5;

        hence ( PolyRedRel ( {g},T)) reduces ((f *' g),( 0_ (n,L))) by REWRITE1: 12;

      end;

      then

       A7: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A7, A2);

      hence thesis by A1;

    end;

    begin

    theorem :: GROEB_3:52

    

     Th52: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L st (( HT (p1,T)),( HT (p2,T))) are_disjoint holds for b1,b2 be bag of n st b1 in ( Support ( Red (p1,T))) & b2 in ( Support ( Red (p2,T))) holds not ((( HT (p1,T)) + b2) = (( HT (p2,T)) + b1))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L;

      assume

       A1: (( HT (p1,T)),( HT (p2,T))) are_disjoint ;

      

       A2: ( Support ( Red (p1,T))) c= ( Support p1) & ( Support ( Red (p2,T))) c= ( Support p2) by TERMORD: 35;

      let b1,b2 be bag of n;

      assume that

       A3: b1 in ( Support ( Red (p1,T))) and

       A4: b2 in ( Support ( Red (p2,T)));

      now

        assume b1 = ( HT (p1,T));

        then (( Red (p1,T)) . b1) = ( 0. L) by TERMORD: 39;

        hence contradiction by A3, POLYNOM1:def 4;

      end;

      hence thesis by A1, A3, A4, A2, Lm5;

    end;

    theorem :: GROEB_3:53

    

     Th53: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L st (( HT (p1,T)),( HT (p2,T))) are_disjoint holds ( S-Poly (p1,p2,T)) = ((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T))))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L;

      assume (( HT (p1,T)),( HT (p2,T))) are_disjoint ;

      then ( lcm (( HT (p1,T)),( HT (p2,T)))) = (( HT (p1,T)) + ( HT (p2,T))) by GROEB_2: 5;

      

      hence ( S-Poly (p1,p2,T)) = ((( HC (p2,T)) * (((( HT (p1,T)) + ( HT (p2,T))) / ( HT (p1,T))) *' p1)) - (( HC (p1,T)) * (((( HT (p1,T)) + ( HT (p2,T))) / ( HT (p2,T))) *' p2))) by GROEB_2:def 4

      .= ((( HC (p2,T)) * (( HT (p2,T)) *' p1)) - (( HC (p1,T)) * (((( HT (p1,T)) + ( HT (p2,T))) / ( HT (p2,T))) *' p2))) by Th1

      .= ((( HC (p2,T)) * (( HT (p2,T)) *' p1)) - (( HC (p1,T)) * (( HT (p1,T)) *' p2))) by Th1

      .= ((( HC (p2,T)) * (( HT (p2,T)) *' (( HM (p1,T)) + ( Red (p1,T))))) - (( HC (p1,T)) * (( HT (p1,T)) *' p2))) by TERMORD: 38

      .= ((( HC (p2,T)) * (( HT (p2,T)) *' (( HM (p1,T)) + ( Red (p1,T))))) - (( HC (p1,T)) * (( HT (p1,T)) *' (( HM (p2,T)) + ( Red (p2,T)))))) by TERMORD: 38

      .= ((( Monom (( HC (p2,T)),( HT (p2,T)))) *' (( HM (p1,T)) + ( Red (p1,T)))) - (( HC (p1,T)) * (( HT (p1,T)) *' (( HM (p2,T)) + ( Red (p2,T)))))) by POLYRED: 22

      .= ((( Monom (( HC (p2,T)),( HT (p2,T)))) *' (( HM (p1,T)) + ( Red (p1,T)))) - (( Monom (( HC (p1,T)),( HT (p1,T)))) *' (( HM (p2,T)) + ( Red (p2,T))))) by POLYRED: 22

      .= ((( HM (p2,T)) *' (( HM (p1,T)) + ( Red (p1,T)))) - (( Monom (( HC (p1,T)),( HT (p1,T)))) *' (( HM (p2,T)) + ( Red (p2,T))))) by TERMORD:def 8

      .= ((( HM (p2,T)) *' (( HM (p1,T)) + ( Red (p1,T)))) - (( HM (p1,T)) *' (( HM (p2,T)) + ( Red (p2,T))))) by TERMORD:def 8

      .= (((( HM (p2,T)) *' ( HM (p1,T))) + (( HM (p2,T)) *' ( Red (p1,T)))) - (( HM (p1,T)) *' (( HM (p2,T)) + ( Red (p2,T))))) by POLYNOM1: 26

      .= (((( HM (p2,T)) *' ( HM (p1,T))) + (( HM (p2,T)) *' ( Red (p1,T)))) - ((( HM (p1,T)) *' ( HM (p2,T))) + (( HM (p1,T)) *' ( Red (p2,T))))) by POLYNOM1: 26

      .= (((( HM (p2,T)) *' ( HM (p1,T))) + (( HM (p2,T)) *' ( Red (p1,T)))) + ( - ((( HM (p1,T)) *' ( HM (p2,T))) + (( HM (p1,T)) *' ( Red (p2,T)))))) by POLYNOM1:def 7

      .= (((( HM (p2,T)) *' ( HM (p1,T))) + (( HM (p2,T)) *' ( Red (p1,T)))) + (( - (( HM (p1,T)) *' ( HM (p2,T)))) + ( - (( HM (p1,T)) *' ( Red (p2,T)))))) by POLYRED: 1

      .= ((( HM (p2,T)) *' ( Red (p1,T))) + ((( HM (p2,T)) *' ( HM (p1,T))) + (( - (( HM (p1,T)) *' ( HM (p2,T)))) + ( - (( HM (p1,T)) *' ( Red (p2,T))))))) by POLYNOM1: 21

      .= ((( HM (p2,T)) *' ( Red (p1,T))) + (((( HM (p2,T)) *' ( HM (p1,T))) + ( - (( HM (p1,T)) *' ( HM (p2,T))))) + ( - (( HM (p1,T)) *' ( Red (p2,T)))))) by POLYNOM1: 21

      .= ((( HM (p2,T)) *' ( Red (p1,T))) + (( 0_ (n,L)) + ( - (( HM (p1,T)) *' ( Red (p2,T)))))) by POLYRED: 3

      .= ((( HM (p2,T)) *' ( Red (p1,T))) + ( - (( HM (p1,T)) *' ( Red (p2,T))))) by POLYRED: 2

      .= ((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))) by POLYNOM1:def 7;

    end;

    theorem :: GROEB_3:54

    

     Th54: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L st (( HT (p1,T)),( HT (p2,T))) are_disjoint holds ( S-Poly (p1,p2,T)) = ((( Red (p1,T)) *' p2) - (( Red (p2,T)) *' p1))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L;

      reconsider r1 = ( - ( Red (p1,T))), r2 = ( - ( Red (p2,T))) as Polynomial of n, L;

      (r2 *' ( Red (p1,T))) = ( - (( Red (p2,T)) *' ( Red (p1,T)))) by POLYRED: 6

      .= (r1 *' ( Red (p2,T))) by POLYRED: 6;

      then

       A1: ((r2 *' ( Red (p1,T))) + ( - (r1 *' ( Red (p2,T))))) = ( 0_ (n,L)) by POLYRED: 3;

      assume (( HT (p1,T)),( HT (p2,T))) are_disjoint ;

      

      hence ( S-Poly (p1,p2,T)) = ((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))) by Th53

      .= (((p2 - ( Red (p2,T))) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))) by Th15

      .= (((p2 - ( Red (p2,T))) *' ( Red (p1,T))) - ((p1 - ( Red (p1,T))) *' ( Red (p2,T)))) by Th15

      .= (((p2 + ( - ( Red (p2,T)))) *' ( Red (p1,T))) - ((p1 - ( Red (p1,T))) *' ( Red (p2,T)))) by POLYNOM1:def 7

      .= (((p2 + ( - ( Red (p2,T)))) *' ( Red (p1,T))) - ((p1 + ( - ( Red (p1,T)))) *' ( Red (p2,T)))) by POLYNOM1:def 7

      .= (((p2 *' ( Red (p1,T))) + (r2 *' ( Red (p1,T)))) - ((p1 + ( - ( Red (p1,T)))) *' ( Red (p2,T)))) by POLYNOM1: 26

      .= (((p2 *' ( Red (p1,T))) + (r2 *' ( Red (p1,T)))) - ((p1 *' ( Red (p2,T))) + (r1 *' ( Red (p2,T))))) by POLYNOM1: 26

      .= (((p2 *' ( Red (p1,T))) + (r2 *' ( Red (p1,T)))) + ( - ((p1 *' ( Red (p2,T))) + (r1 *' ( Red (p2,T)))))) by POLYNOM1:def 7

      .= (((p2 *' ( Red (p1,T))) + (r2 *' ( Red (p1,T)))) + (( - (p1 *' ( Red (p2,T)))) + ( - (r1 *' ( Red (p2,T)))))) by POLYRED: 1

      .= ((p2 *' ( Red (p1,T))) + ((r2 *' ( Red (p1,T))) + (( - (r1 *' ( Red (p2,T)))) + ( - (p1 *' ( Red (p2,T))))))) by POLYNOM1: 21

      .= ((p2 *' ( Red (p1,T))) + (( 0_ (n,L)) + ( - (p1 *' ( Red (p2,T)))))) by A1, POLYNOM1: 21

      .= ((p2 *' ( Red (p1,T))) + ( - (p1 *' ( Red (p2,T))))) by POLYRED: 2

      .= ((( Red (p1,T)) *' p2) - (( Red (p2,T)) *' p1)) by POLYNOM1:def 7;

    end;

    theorem :: GROEB_3:55

    

     Th55: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be non-zero Polynomial of n, L st (( HT (p1,T)),( HT (p2,T))) are_disjoint & ( Red (p1,T)) is non-zero & ( Red (p2,T)) is non-zero holds ( PolyRedRel ( {p1},T)) reduces (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))),(p2 *' ( Red (p1,T))))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be non-zero Polynomial of n, L;

      assume that

       A1: (( HT (p1,T)),( HT (p2,T))) are_disjoint and

       A2: ( Red (p1,T)) is non-zero & ( Red (p2,T)) is non-zero;

      reconsider red1 = ( Red (p1,T)), red2 = ( Red (p2,T)) as non-zero Polynomial of n, L by A2;

      set j = ( card ( Support p2));

      defpred P[ Nat] means for m be Element of NAT st m <= ( card ( Support p2)) & ( card ( Support ( Low (p2,T,m)))) = $1 holds ( PolyRedRel ( {p1},T)) reduces (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))),(((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))));

      now

        assume j = 0 ;

        then ( Support p2) = {} ;

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

        hence contradiction by POLYNOM7:def 1;

      end;

      then

       A3: 1 <= j by NAT_1: 14;

      then (1 - 1) <= (j - 1) by XREAL_1: 9;

      then

      reconsider j9 = (j - 1) as Element of NAT by INT_1: 3;

      

       A4: (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,1))))) + (( Red (p1,T)) *' ( Low (p2,T,1)))) = (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' (( Red (p2,T)) - ( Red (p2,T))))) + (( Red (p1,T)) *' ( Low (p2,T,1)))) by Th36

      .= (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( 0_ (n,L)))) + (( Red (p1,T)) *' ( Low (p2,T,1)))) by POLYNOM1: 24

      .= (((( HM (p2,T)) *' ( Red (p1,T))) - ( 0_ (n,L))) + (( Red (p1,T)) *' ( Low (p2,T,1)))) by POLYRED: 5

      .= ((( HM (p2,T)) *' ( Red (p1,T))) + (( Red (p1,T)) *' ( Low (p2,T,1)))) by POLYRED: 4

      .= ((( HM (p2,T)) *' ( Red (p1,T))) + (( Red (p1,T)) *' ( Red (p2,T)))) by Th36

      .= ((( HM (p2,T)) + ( Red (p2,T))) *' ( Red (p1,T))) by POLYNOM1: 26

      .= (p2 *' ( Red (p1,T))) by TERMORD: 38;

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

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

      then ( HT (p2,T)) in ( Support p2) by TERMORD:def 6;

      then for t be object holds t in {( HT (p2,T))} implies t in ( Support p2) by TARSKI:def 1;

      then

       A5: {( HT (p2,T))} c= ( Support p2);

      

       A6: ( card ( Support red2)) = ( card (( Support p2) \ {( HT (p2,T))})) by TERMORD: 36

      .= (( card ( Support p2)) - ( card {( HT (p2,T))})) by A5, CARD_2: 44

      .= (j - 1) by CARD_2: 42;

      then

       A7: ( card ( Support ( Low (p2,T,1)))) = j9 by Th36;

      

       A8: for k be Element of NAT st 0 <= k & k < j9 holds P[k] implies P[(k + 1)]

      proof

        let k be Element of NAT ;

        assume that 0 <= k and

         A9: k < j9;

        now

          assume

           A10: P[k];

          now

            ( HT ((( HM (p2,T)) *' red1),T)) = (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) & ( HC ((( HM (p2,T)) *' red1),T)) <> ( 0. L) by TERMORD: 31;

            then

             A11: ((( HM (p2,T)) *' red1) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) <> ( 0. L) by TERMORD:def 7;

            

             A12: ( Support ( Red (p2,T))) c= ( Support p2) by TERMORD: 35;

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

            then

             A13: ( Support red2) <> {} by POLYNOM7: 1;

            let m be Element of NAT ;

            assume that

             A14: m <= ( card ( Support p2)) and

             A15: ( card ( Support ( Low (p2,T,m)))) = (k + 1);

            set m9 = (m + 1);

            now

              assume m = ( card ( Support p2));

              then ( Low (p2,T,m)) = ( 0_ (n,L)) by Th35;

              hence contradiction by A15, CARD_1: 27, POLYNOM7: 1;

            end;

            then

             A16: m < ( card ( Support p2)) by A14, XXREAL_0: 1;

            then ( card (( Support ( Low (p2,T,m))) \ ( Support ( Low (p2,T,m9))))) = (( card ( Support ( Low (p2,T,m)))) - ( card ( Support ( Low (p2,T,m9))))) by Th41, CARD_2: 44;

            

            then

             A17: ((k + 1) - ( card ( Support ( Low (p2,T,m9))))) = ( card {( HT (( Low (p2,T,m)),T))}) by A15, A16, Th42

            .= 1 by CARD_1: 30;

            set f = (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m9))))) + (( Red (p1,T)) *' ( Low (p2,T,m9))));

            

             A18: (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) is Element of ( Bags n) by PRE_POLY:def 12;

            

             A19: m9 <= ( card ( Support p2)) by A16, NAT_1: 13;

            now

              

               A20: ( Support (red1 *' ( Low (p2,T,m9)))) c= { (s + t) where s,t be Element of ( Bags n) : s in ( Support red1) & t in ( Support ( Low (p2,T,m9))) } by TERMORD: 30;

              assume (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) in ( Support (red1 *' ( Low (p2,T,m9))));

              then (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) in { (s + t) where s,t be Element of ( Bags n) : s in ( Support red1) & t in ( Support ( Low (p2,T,m9))) } by A20;

              then

              consider s,t be Element of ( Bags n) such that

               A21: (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) = (s + t) and

               A22: s in ( Support red1) and

               A23: t in ( Support ( Low (p2,T,m9)));

              

               A24: t < (( HT (p2,T)),T)

              proof

                now

                  per cases ;

                    case m9 = ( card ( Support p2));

                    then ( Low (p2,T,m9)) = ( 0_ (n,L)) by Th35;

                    hence contradiction by A23, POLYNOM7: 1;

                  end;

                    case

                     A25: m9 <> ( card ( Support p2));

                    

                     A26: t <= (( HT (( Low (p2,T,m9)),T)),T) by A23, TERMORD:def 6;

                    m9 < ( card ( Support p2)) by A19, A25, XXREAL_0: 1;

                    hence thesis by A26, Th3, Th39;

                  end;

                end;

                hence thesis;

              end;

              s <= (( HT (red1,T)),T) by A22, TERMORD:def 6;

              then (s + t) < ((( HT (p2,T)) + ( HT (red1,T))),T) by A24, Th5;

              then (s + t) < ((( HT (( HM (p2,T)),T)) + ( HT (red1,T))),T) by TERMORD: 26;

              hence contradiction by A21, TERMORD:def 3;

            end;

            then

             A27: ((red1 *' ( Low (p2,T,m9))) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) = ( 0. L) by A18, POLYNOM1:def 4;

            

             A28: 1 <= m9 by NAT_1: 14;

            now

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

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

              then

               A29: ( HT (( HM (p2,T)),T)) = ( HT (p2,T)) & ( HT (red1,T)) in ( Support red1) by TERMORD: 26, TERMORD:def 6;

              

               A30: ( Support (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9))))) c= { (s + t) where s,t be Element of ( Bags n) : s in ( Support ( HM (p1,T))) & t in ( Support (red2 - ( Low (p2,T,m9)))) } by TERMORD: 30;

              assume (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) in ( Support (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))));

              then

               A31: (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) in { (s + t) where s,t be Element of ( Bags n) : s in ( Support ( HM (p1,T))) & t in ( Support (red2 - ( Low (p2,T,m9)))) } by A30;

              (red2 - ( Low (p2,T,m9))) = (red2 + ( - ( Low (p2,T,m9)))) & ( Support ( - ( Low (p2,T,m9)))) = ( Support ( Low (p2,T,m9))) by GROEB_1: 5, POLYNOM1:def 7;

              then

               A32: ( Support (red2 - ( Low (p2,T,m9)))) c= (( Support red2) \/ ( Support ( Low (p2,T,m9)))) by POLYNOM1: 20;

              consider s,t be Element of ( Bags n) such that

               A33: (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) = (s + t) and

               A34: s in ( Support ( HM (p1,T))) and

               A35: t in ( Support (red2 - ( Low (p2,T,m9)))) by A31;

              

               A36: ( Support ( Low (p2,T,m9))) c= ( Support red2) by A19, A28, Th27;

              

               A37: t in ( Support red2)

              proof

                now

                  per cases by A35, A32, XBOOLE_0:def 3;

                    case t in ( Support red2);

                    hence thesis;

                  end;

                    case t in ( Support ( Low (p2,T,m9)));

                    hence thesis by A36;

                  end;

                end;

                hence thesis;

              end;

              ( HM (p1,T)) <> ( 0_ (n,L)) by POLYNOM7:def 1;

              then ( Support ( HM (p1,T))) <> {} by POLYNOM7: 1;

              then ( Support ( HM (p1,T))) = {( HT (p1,T))} by TERMORD: 21;

              then s = ( HT (p1,T)) by A34, TARSKI:def 1;

              hence contradiction by A1, A33, A29, A37, Th52;

            end;

            then ((( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) = ( 0. L) by A18, POLYNOM1:def 4;

            then

             A38: ( - ((( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T))))) = ( 0. L) by RLVECT_1: 12;

            

             A39: ( Support ( Low (p2,T,m9))) = ( Lower_Support (p2,T,m9)) by A19, Lm3;

            now

              assume

               A40: ( HT (red2,T)) in ( Support ( Low (p2,T,m9)));

               A41:

              now

                let t be object;

                assume

                 A42: t in ( Support red2);

                then

                reconsider t9 = t as bag of n;

                ( Support red2) c= ( Support p2) & t9 <= (( HT (red2,T)),T) by A42, TERMORD: 35, TERMORD:def 6;

                hence t in ( Support ( Low (p2,T,m9))) by A19, A39, A40, A42, Th24;

              end;

              ( Support ( Low (p2,T,m9))) c= ( Support red2) by A19, A28, Th27;

              then for t be object holds t in ( Support ( Low (p2,T,m9))) implies t in ( Support red2);

              hence contradiction by A6, A9, A17, A41, TARSKI: 2;

            end;

            then ( Low (p2,T,m9)) <> red2 by A13, TERMORD:def 6;

            then (( Red (p2,T)) - ( Low (p2,T,m9))) <> ( 0_ (n,L)) by Th12;

            then

            reconsider z1 = (( Red (p2,T)) - ( Low (p2,T,m9))) as non-zero Polynomial of n, L by POLYNOM7:def 1;

            reconsider z = (( HM (p1,T)) *' z1) as non-zero Polynomial of n, L;

            z1 = (( Red (p2,T)) + ( - ( Low (p2,T,m9)))) by POLYNOM1:def 7;

            then ( Support z1) c= (( Support ( Red (p2,T))) \/ ( Support ( - ( Low (p2,T,m9))))) by POLYNOM1: 20;

            then

             A43: ( Support z1) c= (( Support ( Red (p2,T))) \/ ( Support ( Low (p2,T,m9)))) by GROEB_1: 5;

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

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

            then

            reconsider w = (( card ( Support z)) - 1) as Element of NAT by INT_1: 5, NAT_1: 14;

            reconsider lowzw = ( Low (z,T,w)) as non-zero Monomial of n, L by Th37;

            set b = ( term lowzw);

            set s = (b / ( HT (p1,T)));

            

             A44: ( Support (( HM (p1,T)) *' z1)) c= { (t9 + t) where t9,t be Element of ( Bags n) : t9 in ( Support ( HM (p1,T))) & t in ( Support z1) } by TERMORD: 30;

            ( card ( Support z)) = (w + 1);

            then

             A45: w < ( card ( Support z)) by NAT_1: 16;

            then

             A46: ( Support lowzw) c= ( Support z) by Th26;

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

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

            then ( Support lowzw) = {b} by POLYNOM7: 7;

            then

             A47: b in ( Support lowzw) by TARSKI:def 1;

            then b in ( Support (( HM (p1,T)) *' z1)) by A46;

            then b in { (t9 + t) where t9,t be Element of ( Bags n) : t9 in ( Support ( HM (p1,T))) & t in ( Support z1) } by A44;

            then

            consider t9,t be Element of ( Bags n) such that

             A48: b = (t9 + t) and

             A49: t9 in ( Support ( HM (p1,T))) and

             A50: t in ( Support z1);

            ( HM (p1,T)) <> ( 0_ (n,L)) by POLYNOM7:def 1;

            then ( Support ( HM (p1,T))) <> {} by POLYNOM7: 1;

            

            then ( Support ( HM (p1,T))) = {( term ( HM (p1,T)))} by POLYNOM7: 7

            .= {( HT (p1,T))} by TERMORD: 22;

            then

             A51: t9 = ( HT (p1,T)) by A49, TARSKI:def 1;

            then

             A52: ( HT (p1,T)) divides b by A48, PRE_POLY: 50;

            then

             A53: (s + ( HT (p1,T))) = b by GROEB_2:def 1;

            

             A54: s = ((s + ( HT (p1,T))) -' ( HT (p1,T))) by PRE_POLY: 48

            .= t by A48, A51, A53, PRE_POLY: 48;

            (( Support ( Red (p2,T))) \/ ( Support ( Low (p2,T,m9)))) c= (( Support ( Red (p2,T))) \/ ( Support ( Red (p2,T)))) by A19, A28, Th27, XBOOLE_1: 9;

            then

             A55: ( Support z1) c= ( Support red2) by A43;

            then

             A56: s in ( Support ( Red (p2,T))) by A50, A54;

            then s in (( Support p2) \ {( HT (p2,T))}) by TERMORD: 36;

            then not s in {( HT (p2,T))} by XBOOLE_0:def 5;

            then

             A57: s <> ( HT (p2,T)) by TARSKI:def 1;

            then

             A58: (( Red (p2,T)) . s) = (p2 . s) by A56, A12, TERMORD: 40;

             A59:

            now

              assume s in ( Support ( Low (p2,T,m9)));

              then

               A60: (p2 . s) = (( Low (p2,T,m9)) . s) by Th16;

              ((( Red (p2,T)) - ( Low (p2,T,m9))) . s) = ((( Red (p2,T)) + ( - ( Low (p2,T,m9)))) . s) by POLYNOM1:def 7

              .= ((( Red (p2,T)) . s) + (( - ( Low (p2,T,m9))) . s)) by POLYNOM1: 15

              .= ((( Red (p2,T)) . s) + ( - (( Low (p2,T,m9)) . s))) by POLYNOM1: 17

              .= ( 0. L) by A58, A60, RLVECT_1: 5;

              hence contradiction by A50, A54, POLYNOM1:def 4;

            end;

            

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

             A62:

            now

              assume ((( Red (p1,T)) *' ( Low (p2,T,m9))) . b) <> ( 0. L);

              then

               A63: b in ( Support (( Red (p1,T)) *' ( Low (p2,T,m9)))) by A61, POLYNOM1:def 4;

              ( Support (( Red (p1,T)) *' ( Low (p2,T,m9)))) c= { (u + v) where u,v be Element of ( Bags n) : u in ( Support ( Red (p1,T))) & v in ( Support ( Low (p2,T,m9))) } by TERMORD: 30;

              then b in { (u + v) where u,v be Element of ( Bags n) : u in ( Support ( Red (p1,T))) & v in ( Support ( Low (p2,T,m9))) } by A63;

              then

              consider t9,t be Element of ( Bags n) such that

               A64: b = (t9 + t) and

               A65: t9 in ( Support ( Red (p1,T))) and

               A66: t in ( Support ( Low (p2,T,m9)));

              

               A67: (s + ( HT (p1,T))) = (t9 + t) by A52, A64, GROEB_2:def 1;

              now

                assume s < (t,T);

                then

                 A68: s <= (t,T) by TERMORD:def 3;

                t in ( Lower_Support (p2,T,m9)) by A19, A66, Lm3;

                then s in ( Lower_Support (p2,T,m9)) by A19, A56, A12, A68, Th24;

                hence contradiction by A19, A59, Lm3;

              end;

              then

               A69: t <= (s,T) by TERMORD: 5;

              ( Support ( Red (p1,T))) = (( Support p1) \ {( HT (p1,T))}) by TERMORD: 36;

              then not t9 in {( HT (p1,T))} by A65, XBOOLE_0:def 5;

              then

               A70: t9 <> ( HT (p1,T)) by TARSKI:def 1;

              ( Support ( Red (p1,T))) c= ( Support p1) by TERMORD: 35;

              then t9 <= (( HT (p1,T)),T) by A65, TERMORD:def 6;

              then t9 < (( HT (p1,T)),T) by A70, TERMORD:def 3;

              then (t + t9) < ((s + ( HT (p1,T))),T) by A69, Th6;

              hence contradiction by A67, TERMORD:def 3;

            end;

             A71:

            now

              ( HM (p2,T)) <> ( 0_ (n,L)) by POLYNOM7:def 1;

              then

               A72: ( Support ( HM (p2,T))) <> {} by POLYNOM7: 1;

              then ( HT (( HM (p2,T)),T)) in ( Support ( HM (p2,T))) by TERMORD:def 6;

              then

               A73: ( HT (p2,T)) in ( Support ( HM (p2,T))) by TERMORD: 26;

              

               A74: ( Support (( HM (p2,T)) *' ( Red (p1,T)))) c= { (u + v) where u,v be Element of ( Bags n) : u in ( Support ( HM (p2,T))) & v in ( Support ( Red (p1,T))) } by TERMORD: 30;

              assume b in ( Support (( HM (p2,T)) *' ( Red (p1,T))));

              then b in { (u + v) where u,v be Element of ( Bags n) : u in ( Support ( HM (p2,T))) & v in ( Support ( Red (p1,T))) } by A74;

              then

              consider t9,t be Element of ( Bags n) such that

               A75: b = (t9 + t) and

               A76: t9 in ( Support ( HM (p2,T))) and

               A77: t in ( Support ( Red (p1,T)));

              ex x be bag of n st ( Support ( HM (p2,T))) = {x} by A72, POLYNOM7: 6;

              then ( Support ( HM (p2,T))) = {( HT (p2,T))} by A73, TARSKI:def 1;

              then t9 = ( HT (p2,T)) by A76, TARSKI:def 1;

              hence contradiction by A1, A55, A50, A53, A54, A75, A77, Th52;

            end;

            set g = (f - (((f . b) / ( HC (p1,T))) * (s *' p1)));

            

             A78: (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) is Element of ( Bags n) by PRE_POLY:def 12;

            

             A79: (f . b) = ((((( HM (p2,T)) *' red1) + ( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))))) + (red1 *' ( Low (p2,T,m9)))) . b) by POLYNOM1:def 7

            .= ((((( HM (p2,T)) *' red1) + ( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))))) . b) + ( 0. L)) by A62, POLYNOM1: 15

            .= (((( HM (p2,T)) *' red1) + ( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))))) . b) by RLVECT_1:def 4

            .= (((( HM (p2,T)) *' red1) . b) + (( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9))))) . b)) by POLYNOM1: 15

            .= (( 0. L) + (( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9))))) . b)) by A61, A71, POLYNOM1:def 4

            .= (( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9))))) . b) by RLVECT_1:def 4

            .= ( - ((( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))) . b)) by POLYNOM1: 17;

            w = (( card ( Support z1)) - 1) by Th10;

            then

            reconsider lowz1w = ( Low (z1,T,w)) as non-zero Monomial of n, L by Th37;

            (w + 1) = ((( card ( Support z1)) - 1) + 1) by Th10;

            then

             A80: w <= ( card ( Support z1)) by NAT_1: 13;

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

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

            then

             A81: ( Support lowz1w) = {( term lowz1w)} by POLYNOM7: 7;

            ( card ( Support z)) = ( card ( Support z1)) by Th10;

            

            then (s + ( HT (p1,T))) = ( term (( HM (p1,T)) *' lowz1w)) by A45, A53, Th44

            .= (( term ( HM (p1,T))) + ( term lowz1w)) by Th7

            .= (( HT (p1,T)) + ( term lowz1w)) by TERMORD: 22;

            

            then

             A82: s = ((( HT (p1,T)) + ( term lowz1w)) -' ( HT (p1,T))) by PRE_POLY: 48

            .= ( term lowz1w) by PRE_POLY: 48;

            then s in ( Support lowz1w) by A81, TARSKI:def 1;

            then

             A83: s in ( Lower_Support (z1,T,w)) by A80, Lm3;

            ( Monom ((p2 . s),s)) = ( HM (( Low (p2,T,m)),T))

            proof

               A84:

              now

                let t be bag of n;

                assume

                 A85: t in ( Support z1);

                now

                  assume

                   A86: t < (s,T);

                  then t <= (s,T) by TERMORD:def 3;

                  then t in ( Lower_Support (z1,T,w)) by A80, A83, A85, Th24;

                  then t in ( Support lowz1w) by A80, Lm3;

                  then t = ( term lowz1w) by A81, TARSKI:def 1;

                  hence contradiction by A82, A86, TERMORD:def 3;

                end;

                hence s <= (t,T) by TERMORD: 5;

              end;

              set r = ( HT (( Low (p2,T,m)),T));

              (( Support ( Low (p2,T,m))) \ ( Support ( Low (p2,T,m9)))) = {( HT (( Low (p2,T,m)),T))} by A16, Th42;

              then

               A87: r in (( Support ( Low (p2,T,m))) \ ( Support ( Low (p2,T,m9)))) by TARSKI:def 1;

              then

               A88: not r in ( Support ( Low (p2,T,m9))) by XBOOLE_0:def 5;

              

               A89: ((( Red (p2,T)) - ( Low (p2,T,m9))) . r) = ((( Red (p2,T)) + ( - ( Low (p2,T,m9)))) . r) by POLYNOM1:def 7

              .= ((( Red (p2,T)) . r) + (( - ( Low (p2,T,m9))) . r)) by POLYNOM1: 15

              .= ((( Red (p2,T)) . r) + ( - (( Low (p2,T,m9)) . r))) by POLYNOM1: 17

              .= ((( Red (p2,T)) . r) + ( - ( 0. L))) by A88, POLYNOM1:def 4

              .= ((( Red (p2,T)) . r) + ( 0. L)) by RLVECT_1: 12

              .= (( Red (p2,T)) . r) by RLVECT_1:def 4;

              

               A90: r in ( Support ( Low (p2,T,m))) by A87, XBOOLE_0:def 5;

              then

               A91: r in ( Lower_Support (p2,T,m)) by A14, Lm3;

              

               A92: ( Support ( Low (p2,T,m))) c= ( Support p2) by A14, Th26;

              now

                assume

                 A93: r = ( HT (p2,T));

                 A94:

                now

                  let u be object;

                  assume

                   A95: u in ( Support p2);

                  then

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

                  u9 <= (r,T) by A93, A95, TERMORD:def 6;

                  then u9 in ( Lower_Support (p2,T,m)) by A14, A91, A95, Th24;

                  hence u in ( Support ( Low (p2,T,m))) by A14, Lm3;

                end;

                for u be object holds u in ( Support ( Low (p2,T,m))) implies u in ( Support p2) by A92;

                then (k + 1) = j by A15, A94, TARSKI: 2;

                hence contradiction by A9;

              end;

              then

               A96: not r in {( HT (p2,T))} by TARSKI:def 1;

              ( Support ( Red (p2,T))) = (( Support p2) \ {( HT (p2,T))}) by TERMORD: 36;

              then r in ( Support red2) by A90, A92, A96, XBOOLE_0:def 5;

              then (z1 . r) <> ( 0. L) by A89, POLYNOM1:def 4;

              then

               A97: r in ( Support z1) by POLYNOM1:def 4;

              ( Support red2) c= ( Support p2) by TERMORD: 35;

              then s in ( Lower_Support (p2,T,m)) by A14, A56, A84, A91, A97, Th24;

              then

               A98: s in ( Support ( Low (p2,T,m))) by A14, Lm3;

              then s in (( Support ( Low (p2,T,m))) \ ( Support ( Low (p2,T,m9)))) by A59, XBOOLE_0:def 5;

              then s in {( HT (( Low (p2,T,m)),T))} by A16, Th42;

              then

               A99: s = ( HT (( Low (p2,T,m)),T)) by TARSKI:def 1;

              

              then

               A100: (( HM (( Low (p2,T,m)),T)) . ( HT (( Low (p2,T,m)),T))) = (( Low (p2,T,m)) . s) by TERMORD: 18

              .= (p2 . s) by A14, A98, Th31;

              ( HC (( Low (p2,T,m)),T)) = (( Low (p2,T,m)) . ( HT (( Low (p2,T,m)),T))) by TERMORD:def 7

              .= (p2 . s) by A100, TERMORD: 18;

              hence thesis by A99, TERMORD:def 8;

            end;

            

            then

             A101: ( Low (p2,T,m)) = (( Monom ((p2 . s),s)) + ( Red (( Low (p2,T,m)),T))) by TERMORD: 38

            .= (( Monom ((p2 . s),s)) + ( Low (p2,T,m9))) by A16, Th43;

            

             A102: ((( HM (p1,T)) *' z1) . b) <> ( 0. L) by A47, A46, POLYNOM1:def 4;

            now

              assume (f . b) = ( 0. L);

              then ((( HM (p1,T)) *' z1) . b) = ( - ( 0. L)) by A79, RLVECT_1: 17;

              hence contradiction by A102, RLVECT_1: 12;

            end;

            then

             A103: p1 <> ( 0_ (n,L)) & b in ( Support f) by A61, POLYNOM1:def 4, POLYNOM7:def 1;

            (f . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) = ((((( HM (p2,T)) *' red1) + ( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))))) + (red1 *' ( Low (p2,T,m9)))) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) by POLYNOM1:def 7

            .= ((((( HM (p2,T)) *' red1) + ( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))))) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) + ( 0. L)) by A27, POLYNOM1: 15

            .= (((( HM (p2,T)) *' red1) + ( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))))) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) by RLVECT_1:def 4

            .= (((( HM (p2,T)) *' red1) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) + (( - (( HM (p1,T)) *' (red2 - ( Low (p2,T,m9))))) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T))))) by POLYNOM1: 15

            .= (((( HM (p2,T)) *' red1) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) + ( 0. L)) by A38, POLYNOM1: 17

            .= ((( HM (p2,T)) *' red1) . (( HT (( HM (p2,T)),T)) + ( HT (red1,T)))) by RLVECT_1:def 4;

            then (( HT (( HM (p2,T)),T)) + ( HT (red1,T))) in ( Support f) by A11, A78, POLYNOM1:def 4;

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

            then f reduces_to (g,p1,b,T) by A53, A103, POLYRED:def 5;

            then

             A104: f reduces_to (g,p1,T) by POLYRED:def 6;

            p1 in {p1} by TARSKI:def 1;

            then f reduces_to (g, {p1},T) by A104, POLYRED:def 7;

            then [f, g] in ( PolyRedRel ( {p1},T)) by POLYRED:def 13;

            then

             A105: ( PolyRedRel ( {p1},T)) reduces (f,g) by REWRITE1: 15;

            m9 <= ( card ( Support p2)) by A16, NAT_1: 13;

            then

             A106: ( PolyRedRel ( {p1},T)) reduces (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))),f) by A10, A17;

            

             A107: ( HT (p1,T)) = ( HT (( HM (p1,T)),T)) by TERMORD: 26

            .= ( term ( HM (p1,T))) by TERMORD: 23;

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

            then

             A108: (( Low (p2,T,m9)) . s) = ( 0. L) by A59, POLYNOM1:def 4;

            

             A109: ( Low (p2,T,m)) = ( - ( - ( Low (p2,T,m)))) by POLYNOM1: 19;

            

             A110: ( Low (p2,T,m9)) = ( - ( - ( Low (p2,T,m9)))) by POLYNOM1: 19;

            ((( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))) . b) = ((( HM (p1,T)) *' (red2 - ( Low (p2,T,m9)))) . (s + ( HT (p1,T)))) by A52, GROEB_2:def 1

            .= ((( HM (p1,T)) . ( HT (p1,T))) * ((red2 - ( Low (p2,T,m9))) . s)) by A107, POLYRED: 7

            .= ((p1 . ( HT (p1,T))) * ((red2 - ( Low (p2,T,m9))) . s)) by TERMORD: 18

            .= (( HC (p1,T)) * ((red2 - ( Low (p2,T,m9))) . s)) by TERMORD:def 7

            .= (( HC (p1,T)) * ((red2 + ( - ( Low (p2,T,m9)))) . s)) by POLYNOM1:def 7

            .= (( HC (p1,T)) * ((red2 . s) + (( - ( Low (p2,T,m9))) . s))) by POLYNOM1: 15

            .= (( HC (p1,T)) * ((p2 . s) + (( - ( Low (p2,T,m9))) . s))) by A56, A12, A57, TERMORD: 40

            .= (( HC (p1,T)) * ((p2 . s) + ( - (( Low (p2,T,m9)) . s)))) by POLYNOM1: 17

            .= (( HC (p1,T)) * ((p2 . s) + ( 0. L))) by A108, RLVECT_1: 12

            .= (( HC (p1,T)) * (p2 . s)) by RLVECT_1:def 4;

            

            then (((f . b) / ( HC (p1,T))) * (s *' p1)) = (((( HC (p1,T)) * ( - (p2 . s))) / ( HC (p1,T))) * (s *' p1)) by A79, VECTSP_1: 9

            .= (((( HC (p1,T)) * ( - (p2 . s))) * (( HC (p1,T)) " )) * (s *' p1))

            .= ((( - (p2 . s)) * (( HC (p1,T)) * (( HC (p1,T)) " ))) * (s *' p1)) by GROUP_1:def 3

            .= ((( - (p2 . s)) * ( 1. L)) * (s *' p1)) by VECTSP_1:def 10

            .= (( - (p2 . s)) * (s *' p1));

            

            then g = (f + ( - (( - (p2 . s)) * (s *' p1)))) by POLYNOM1:def 7

            .= (f + (( - ( - (p2 . s))) * (s *' p1))) by POLYRED: 9

            .= (f + ((p2 . s) * (s *' p1))) by RLVECT_1: 17

            .= (f + (( Monom ((p2 . s),s)) *' p1)) by POLYRED: 22

            .= (f + (( Monom ((p2 . s),s)) *' (( HM (p1,T)) + ( Red (p1,T))))) by TERMORD: 38

            .= (f + ((( Monom ((p2 . s),s)) *' ( HM (p1,T))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T))))) by POLYNOM1: 26

            .= ((((( HM (p2,T)) *' ( Red (p1,T))) + ( - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m9)))))) + (( Red (p1,T)) *' ( Low (p2,T,m9)))) + ((( Monom ((p2 . s),s)) *' ( HM (p1,T))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T))))) by POLYNOM1:def 7

            .= (((((( HM (p2,T)) *' ( Red (p1,T))) + ( - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m9)))))) + (( Red (p1,T)) *' ( Low (p2,T,m9)))) + (( Monom ((p2 . s),s)) *' ( HM (p1,T)))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T)))) by POLYNOM1: 21

            .= (((((( HM (p2,T)) *' ( Red (p1,T))) + ( - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m9)))))) + (( Monom ((p2 . s),s)) *' ( HM (p1,T)))) + (( Red (p1,T)) *' ( Low (p2,T,m9)))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T)))) by POLYNOM1: 21

            .= (((((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' ( - (( Red (p2,T)) - ( Low (p2,T,m9)))))) + (( Monom ((p2 . s),s)) *' ( HM (p1,T)))) + (( Red (p1,T)) *' ( Low (p2,T,m9)))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T)))) by POLYRED: 6

            .= ((((( HM (p2,T)) *' ( Red (p1,T))) + ((( HM (p1,T)) *' ( - (( Red (p2,T)) - ( Low (p2,T,m9))))) + (( Monom ((p2 . s),s)) *' ( HM (p1,T))))) + (( Red (p1,T)) *' ( Low (p2,T,m9)))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T)))) by POLYNOM1: 21

            .= ((((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' (( - (( Red (p2,T)) - ( Low (p2,T,m9)))) + ( Monom ((p2 . s),s))))) + (( Red (p1,T)) *' ( Low (p2,T,m9)))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T)))) by POLYNOM1: 26

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' (( - (( Red (p2,T)) - ( Low (p2,T,m9)))) + ( Monom ((p2 . s),s))))) + ((( Red (p1,T)) *' ( Low (p2,T,m9))) + (( Monom ((p2 . s),s)) *' ( Red (p1,T))))) by POLYNOM1: 21

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' (( - (( Red (p2,T)) - ( Low (p2,T,m9)))) + ( Monom ((p2 . s),s))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by A101, POLYNOM1: 26

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' (( - (( Red (p2,T)) + ( - ( Low (p2,T,m9))))) + ( Monom ((p2 . s),s))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by POLYNOM1:def 7

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' ((( - ( Red (p2,T))) + ( - ( - ( Low (p2,T,m9))))) + ( Monom ((p2 . s),s))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by POLYRED: 1

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' (( - ( Red (p2,T))) + ( - ( - ( Low (p2,T,m))))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by A109, A110, A101, POLYNOM1: 21

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' ( - (( Red (p2,T)) + ( - ( Low (p2,T,m))))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by POLYRED: 1

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + (( HM (p1,T)) *' ( - (( Red (p2,T)) - ( Low (p2,T,m)))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by POLYNOM1:def 7

            .= (((( HM (p2,T)) *' ( Red (p1,T))) + ( - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m)))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by POLYRED: 6

            .= (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) by POLYNOM1:def 7;

            hence ( PolyRedRel ( {p1},T)) reduces (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))),(((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m))))) + (( Red (p1,T)) *' ( Low (p2,T,m))))) by A105, A106, REWRITE1: 16;

          end;

          hence P[(k + 1)];

        end;

        hence thesis;

      end;

      

       A111: P[ 0 ]

      proof

        let m be Element of NAT ;

        assume that m <= ( card ( Support p2)) and

         A112: ( card ( Support ( Low (p2,T,m)))) = 0 ;

        ( Support ( Low (p2,T,m))) = {} by A112;

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

        

        then (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' (( Red (p2,T)) - ( Low (p2,T,m))))) + (( Red (p1,T)) *' ( Low (p2,T,m)))) = (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))) + (( Red (p1,T)) *' ( 0_ (n,L)))) by POLYRED: 4

        .= (((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))) + ( 0_ (n,L))) by POLYRED: 5

        .= ((( HM (p2,T)) *' ( Red (p1,T))) - (( HM (p1,T)) *' ( Red (p2,T)))) by POLYRED: 2;

        hence thesis by REWRITE1: 12;

      end;

      for i be Element of NAT st 0 <= i & i <= j9 holds P[i] from INT_1:sch 7( A111, A8);

      hence thesis by A3, A7, A4;

    end;

    theorem :: GROEB_3:56

    

     Th56: for n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L st (( HT (p1,T)),( HT (p2,T))) are_disjoint holds ( PolyRedRel ( {p1, p2},T)) reduces (( S-Poly (p1,p2,T)),( 0_ (n,L)))

    proof

      let n be Ordinal, T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L;

      assume

       A1: (( HT (p1,T)),( HT (p2,T))) are_disjoint ;

      then

       A2: ( S-Poly (p1,p2,T)) = ((( Red (p1,T)) *' p2) - (( Red (p2,T)) *' p1)) by Th54;

      now

        per cases ;

          case p1 = ( 0_ (n,L));

          then (( Red (p2,T)) *' p1) = ( 0_ (n,L)) & ( Red (p1,T)) = ( 0_ (n,L)) by Th11, POLYNOM1: 28;

          

          then ( S-Poly (p1,p2,T)) = (( 0_ (n,L)) - ( 0_ (n,L))) by A2, POLYNOM1: 28

          .= ( 0_ (n,L)) by POLYRED: 4;

          hence thesis by REWRITE1: 12;

        end;

          case p1 <> ( 0_ (n,L));

          then

          reconsider p1a = p1 as non-zero Polynomial of n, L by POLYNOM7:def 1;

          now

            let u be object;

            assume u in {p2};

            then u = p2 by TARSKI:def 1;

            hence u in {p1, p2} by TARSKI:def 2;

          end;

          then

           A3: {p2} c= {p1, p2};

          then

           A4: ( PolyRedRel ( {p2},T)) c= ( PolyRedRel ( {p1, p2},T)) by GROEB_1: 4;

          now

            let u be object;

            assume u in {p1};

            then u = p1 by TARSKI:def 1;

            hence u in {p1, p2} by TARSKI:def 2;

          end;

          then

           A5: {p1} c= {p1, p2};

          then

           A6: ( PolyRedRel ( {p1},T)) c= ( PolyRedRel ( {p1, p2},T)) by GROEB_1: 4;

          now

            per cases ;

              case p2 = ( 0_ (n,L));

              then (( Red (p1,T)) *' p2) = ( 0_ (n,L)) & ( Red (p2,T)) = ( 0_ (n,L)) by Th11, POLYNOM1: 28;

              

              then ( S-Poly (p1,p2,T)) = (( 0_ (n,L)) - ( 0_ (n,L))) by A2, POLYNOM1: 28

              .= ( 0_ (n,L)) by POLYRED: 4;

              hence thesis by REWRITE1: 12;

            end;

              case p2 <> ( 0_ (n,L));

              then

              reconsider p2a = p2 as non-zero Polynomial of n, L by POLYNOM7:def 1;

              now

                per cases ;

                  case ( Red (p1,T)) = ( 0_ (n,L));

                  then

                   A7: ( S-Poly (p1,p2,T)) = (( 0_ (n,L)) - (( Red (p2,T)) *' p1)) by A2, POLYNOM1: 28;

                  now

                    per cases ;

                      case ( Red (p2,T)) = ( 0_ (n,L));

                      

                      then ( S-Poly (p1,p2,T)) = (( 0_ (n,L)) - ( 0_ (n,L))) by A7, POLYNOM1: 28

                      .= ( 0_ (n,L)) by POLYRED: 4;

                      hence thesis by REWRITE1: 12;

                    end;

                      case ( Red (p2,T)) <> ( 0_ (n,L));

                      then

                      reconsider rp2 = ( Red (p2,T)) as non-zero Polynomial of n, L by POLYNOM7:def 1;

                      ( PolyRedRel ( {p1a},T)) reduces (( - (rp2 *' p1a)),( - ( 0_ (n,L)))) by Th49, Th51;

                      then ( PolyRedRel ( {p1a},T)) reduces (( - (rp2 *' p1a)),( 0_ (n,L))) by Th13;

                      then ( PolyRedRel ( {p1},T)) reduces (( S-Poly (p1,p2,T)),( 0_ (n,L))) by A7, Th14;

                      hence thesis by A5, GROEB_1: 4, REWRITE1: 22;

                    end;

                  end;

                  hence thesis;

                end;

                  case ( Red (p1,T)) <> ( 0_ (n,L));

                  then

                  reconsider rp1 = ( Red (p1,T)) as non-zero Polynomial of n, L by POLYNOM7:def 1;

                  now

                    per cases ;

                      case ( Red (p2,T)) = ( 0_ (n,L));

                      then (( Red (p2,T)) *' p1) = ( 0_ (n,L)) by POLYNOM1: 28;

                      

                      then

                       A8: ( S-Poly (p1,p2,T)) = ((( Red (p1,T)) *' p2) - ( 0_ (n,L))) by A1, Th54

                      .= (( Red (p1,T)) *' p2) by POLYRED: 4;

                      ( PolyRedRel ( {p2a},T)) reduces ((rp1 *' p2a),( 0_ (n,L))) by Th51;

                      hence thesis by A3, A8, GROEB_1: 4, REWRITE1: 22;

                    end;

                      case ( Red (p2,T)) <> ( 0_ (n,L));

                      then

                      reconsider rp2 = ( Red (p2,T)) as non-zero Polynomial of n, L by POLYNOM7:def 1;

                      ( S-Poly (p1,p2,T)) = ((( HM (p2a,T)) *' rp1) - (( HM (p1a,T)) *' rp2)) by A1, Th53;

                      then

                       A9: ( PolyRedRel ( {p1, p2},T)) reduces (( S-Poly (p1,p2,T)),(p2 *' ( Red (p1,T)))) by A1, A6, Th55, REWRITE1: 22;

                      ( PolyRedRel ( {p1, p2},T)) reduces ((rp1 *' p2a),( 0_ (n,L))) by A4, Th51, REWRITE1: 22;

                      hence thesis by A9, REWRITE1: 16;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_3:57

    for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L)) holds G is_Groebner_basis_wrt T implies (for g1,g2 be Polynomial of n, L st g1 in G & g2 in G & not ((( HT (g1,T)),( HT (g2,T))) are_disjoint ) holds ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L))))

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L));

      assume G is_Groebner_basis_wrt T;

      then for g1,g2,h be Polynomial of n, L st g1 in G & g2 in G & h is_a_normal_form_of (( S-Poly (g1,g2,T)),( PolyRedRel (G,T))) holds h = ( 0_ (n,L)) by GROEB_2: 23;

      hence thesis by GROEB_2: 24;

    end;

    theorem :: GROEB_3:58

    for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non trivial doubleLoopStr, G be Subset of ( Polynom-Ring (n,L)) st not (( 0_ (n,L)) in G) holds (for g1,g2 be Polynomial of n, L st g1 in G & g2 in G & not ((( HT (g1,T)),( HT (g2,T))) are_disjoint ) holds ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L)))) implies (for g1,g2,h be Polynomial of n, L st g1 in G & g2 in G & not ((( HT (g1,T)),( HT (g2,T))) are_disjoint ) & h is_a_normal_form_of (( S-Poly (g1,g2,T)),( PolyRedRel (G,T))) holds h = ( 0_ (n,L)))

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non trivial doubleLoopStr, G be Subset of ( Polynom-Ring (n,L));

      assume

       A1: not ( 0_ (n,L)) in G;

      assume

       A2: for g1,g2 be Polynomial of n, L st g1 in G & g2 in G & not (( HT (g1,T)),( HT (g2,T))) are_disjoint holds ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L)));

      for g1,g2 be Polynomial of n, L st g1 in G & g2 in G holds ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L)))

      proof

        let g1,g2 be Polynomial of n, L;

        assume that

         A3: g1 in G and

         A4: g2 in G;

        now

          per cases ;

            case

             A5: (( HT (g1,T)),( HT (g2,T))) are_disjoint ;

            now

              let u be object;

              assume

               A6: u in {g1, g2};

              now

                per cases by A6, TARSKI:def 2;

                  case u = g1;

                  hence u in G by A3;

                end;

                  case u = g2;

                  hence u in G by A4;

                end;

              end;

              hence u in G;

            end;

            then

             A7: {g1, g2} c= G;

            ( PolyRedRel ( {g1, g2},T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L))) by A5, Th56;

            hence thesis by A7, GROEB_1: 4, REWRITE1: 22;

          end;

            case not (( HT (g1,T)),( HT (g2,T))) are_disjoint ;

            hence thesis by A2, A3, A4;

          end;

        end;

        hence thesis;

      end;

      then G is_Groebner_basis_wrt T by A1, GROEB_2: 25;

      hence thesis by GROEB_2: 23;

    end;

    theorem :: GROEB_3:59

    for n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L)) st not (( 0_ (n,L)) in G) holds (for g1,g2,h be Polynomial of n, L st g1 in G & g2 in G & not ((( HT (g1,T)),( HT (g2,T))) are_disjoint ) & h is_a_normal_form_of (( S-Poly (g1,g2,T)),( PolyRedRel (G,T))) holds h = ( 0_ (n,L))) implies G is_Groebner_basis_wrt T

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L));

      assume

       A1: not ( 0_ (n,L)) in G;

      assume

       A2: for g1,g2,h be Polynomial of n, L st g1 in G & g2 in G & not (( HT (g1,T)),( HT (g2,T))) are_disjoint & h is_a_normal_form_of (( S-Poly (g1,g2,T)),( PolyRedRel (G,T))) holds h = ( 0_ (n,L));

      for g1,g2 be Polynomial of n, L st g1 in G & g2 in G holds ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L)))

      proof

        let g1,g2 be Polynomial of n, L;

        assume that

         A3: g1 in G and

         A4: g2 in G;

        now

          per cases ;

            case

             A5: (( HT (g1,T)),( HT (g2,T))) are_disjoint ;

            now

              let u be object;

              assume

               A6: u in {g1, g2};

              now

                per cases by A6, TARSKI:def 2;

                  case u = g1;

                  hence u in G by A3;

                end;

                  case u = g2;

                  hence u in G by A4;

                end;

              end;

              hence u in G;

            end;

            then

             A7: {g1, g2} c= G;

            ( PolyRedRel ( {g1, g2},T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L))) by A5, Th56;

            hence thesis by A7, GROEB_1: 4, REWRITE1: 22;

          end;

            case

             A8: not (( HT (g1,T)),( HT (g2,T))) are_disjoint ;

            ( S-Poly (g1,g2,T)) has_a_normal_form_wrt ( PolyRedRel (G,T))

            proof

              now

                per cases ;

                  case not ( S-Poly (g1,g2,T)) in ( field ( PolyRedRel (G,T)));

                  hence thesis by REWRITE1: 46;

                end;

                  case ( S-Poly (g1,g2,T)) in ( field ( PolyRedRel (G,T)));

                  hence thesis by REWRITE1:def 14;

                end;

              end;

              hence thesis;

            end;

            then

            consider h be object such that

             A9: h is_a_normal_form_of (( S-Poly (g1,g2,T)),( PolyRedRel (G,T))) by REWRITE1:def 11;

            ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),h) by A9, REWRITE1:def 6;

            then

            reconsider h as Polynomial of n, L by Lm1;

            h = ( 0_ (n,L)) by A2, A3, A4, A8, A9;

            hence thesis by A9, REWRITE1:def 6;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1, GROEB_2: 25;

    end;