groeb_2.miz



    begin

    theorem :: GROEB_2:1

    for L be add-associative right_zeroed right_complementable non empty addLoopStr, p be FinSequence of L, n be Element of NAT st for k be Element of NAT st k in ( dom p) & k > n holds (p . k) = ( 0. L) holds ( Sum p) = ( Sum (p | n))

    proof

      let L be add-associative right_zeroed right_complementable non empty addLoopStr, p be FinSequence of L, n be Element of NAT ;

      defpred P[ Nat] means for p be FinSequence of L, n be Element of NAT st ( len p) = $1 & for k be Element of NAT st k in ( dom p) & k > n holds (p . k) = ( 0. L) holds ( Sum p) = ( Sum (p | n));

       A1:

      now

        let k be Nat;

        assume

         A2: P[k];

        now

          let p be FinSequence of L, n be Element of NAT ;

          assume that

           A3: ( len p) = (k + 1) and

           A4: for l be Element of NAT st l in ( dom p) & l > n holds (p . l) = ( 0. L);

          

           A5: ( dom p) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

          set q = (p | ( Seg k));

          reconsider q as FinSequence of L by FINSEQ_1: 18;

          

           A6: k <= ( len p) by A3, NAT_1: 11;

          then

           A7: ( len q) = k by FINSEQ_1: 17;

          k <= (k + 1) & ( dom q) = ( Seg k) by A6, FINSEQ_1: 17, NAT_1: 11;

          then

           A8: ( dom q) c= ( dom p) by A5, FINSEQ_1: 5;

          

           A9: q = (p | k) by FINSEQ_1:def 15;

          

           A10: (q ^ <*(p /. (k + 1))*>) = (q ^ <*(p . (k + 1))*>) by A5, FINSEQ_1: 4, PARTFUN1:def 6

          .= p by A3, FINSEQ_3: 55;

          now

            per cases ;

              case

               A11: k < n;

              

               A12: ( dom (p | n)) = ( dom (p | ( Seg n))) by FINSEQ_1:def 15;

              

               A13: (k + 1) <= n by A11, NAT_1: 13;

               A14:

              now

                let u be object;

                assume

                 A15: u in ( dom p);

                then

                reconsider u9 = u as Element of NAT ;

                

                 A16: u in ( Seg (k + 1)) by A3, A15, FINSEQ_1:def 3;

                then u9 <= (k + 1) by FINSEQ_1: 1;

                then

                 A17: u9 <= n by A13, XXREAL_0: 2;

                1 <= u9 by A16, FINSEQ_1: 1;

                then u9 in ( Seg n) by A17, FINSEQ_1: 1;

                then u9 in (( dom p) /\ ( Seg n)) by A15, XBOOLE_0:def 4;

                hence u in ( dom (p | n)) by A12, RELAT_1: 61;

              end;

              

               A18: for x be object st x in ( dom (p | ( Seg n))) holds ((p | ( Seg n)) . x) = (p . x) by FUNCT_1: 47;

              now

                let u be object;

                assume u in ( dom (p | n));

                then

                 A19: u in ( dom (p | ( Seg n))) by FINSEQ_1:def 15;

                ( dom (p | ( Seg n))) c= ( dom p) by RELAT_1: 60;

                hence u in ( dom p) by A19;

              end;

              then ( dom (p | n)) = ( dom p) by A14, TARSKI: 2;

              then (p | ( Seg n)) = p by A12, A18, FUNCT_1: 2;

              hence ( Sum (p | n)) = ( Sum p) by FINSEQ_1:def 15;

            end;

              case

               A20: n <= k;

               A21:

              now

                let l be Element of NAT ;

                assume that

                 A22: l in ( dom q) and

                 A23: l > n;

                

                 A24: (p . l) = ( 0. L) by A4, A8, A22, A23;

                

                thus (q . l) = (q /. l) by A22, PARTFUN1:def 6

                .= (p /. l) by A9, A22, FINSEQ_4: 70

                .= ( 0. L) by A8, A22, A24, PARTFUN1:def 6;

              end;

              (k + 1) > n by A20, NAT_1: 13;

              

              then

               A25: ( 0. L) = (p . (k + 1)) by A4, A5, FINSEQ_1: 4

              .= (p /. (k + 1)) by A5, FINSEQ_1: 4, PARTFUN1:def 6;

              

              thus ( Sum p) = (( Sum q) + ( Sum <*(p /. (k + 1))*>)) by A10, RLVECT_1: 41

              .= (( Sum q) + (p /. (k + 1))) by RLVECT_1: 44

              .= ( Sum q) by A25, RLVECT_1:def 4

              .= ( Sum (q | n)) by A2, A7, A21

              .= ( Sum (p | n)) by A9, A20, FINSEQ_1: 82;

            end;

          end;

          hence ( Sum p) = ( Sum (p | n));

        end;

        hence P[(k + 1)];

      end;

      

       A26: P[ 0 ] by FINSEQ_1: 58;

      

       A27: for k be Nat holds P[k] from NAT_1:sch 2( A26, A1);

      

       A28: ex k be Element of NAT st ( len p) = k;

      assume for k be Element of NAT st k in ( dom p) & k > n holds (p . k) = ( 0. L);

      hence thesis by A27, A28;

    end;

    theorem :: GROEB_2:2

    for L be add-associative right_zeroed Abelian non empty addLoopStr, f be FinSequence of L, i,j be Element of NAT holds ( Sum ( Swap (f,i,j))) = ( Sum f)

    proof

      let L be add-associative right_zeroed Abelian non empty addLoopStr, f be FinSequence of L, i,j be Element of NAT ;

      per cases ;

        suppose not (1 <= i & i <= ( len f) & 1 <= j & j <= ( len f));

        hence thesis by FINSEQ_7:def 2;

      end;

        suppose

         A1: 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f);

        then j in ( Seg ( len f)) by FINSEQ_1: 1;

        then

         A2: j in ( dom f) by FINSEQ_1:def 3;

        i in ( Seg ( len f)) by A1, FINSEQ_1: 1;

        then

         A3: i in ( dom f) by FINSEQ_1:def 3;

        now

          per cases by XXREAL_0: 1;

            case i = j;

            hence thesis by FINSEQ_7: 19;

          end;

            case

             A4: i < j;

            then ( Swap (f,i,j)) = (((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)) by A1, FINSEQ_7: 27;

            

            then

             A5: ( Sum ( Swap (f,i,j))) = (( Sum ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>)) + ( Sum (f /^ j))) by RLVECT_1: 41

            .= ((( Sum (((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1)))) + ( Sum <*(f /. i)*>)) + ( Sum (f /^ j))) by RLVECT_1: 41

            .= (((( Sum ((f | (i -' 1)) ^ <*(f /. j)*>)) + ( Sum ((f /^ i) | ((j -' i) -' 1)))) + ( Sum <*(f /. i)*>)) + ( Sum (f /^ j))) by RLVECT_1: 41

            .= ((((( Sum (f | (i -' 1))) + ( Sum <*(f /. j)*>)) + ( Sum ((f /^ i) | ((j -' i) -' 1)))) + ( Sum <*(f /. i)*>)) + ( Sum (f /^ j))) by RLVECT_1: 41

            .= ((((( Sum (f | (i -' 1))) + ( Sum <*(f /. j)*>)) + ( Sum <*(f /. i)*>)) + ( Sum ((f /^ i) | ((j -' i) -' 1)))) + ( Sum (f /^ j))) by RLVECT_1:def 3

            .= ((((( Sum (f | (i -' 1))) + ( Sum <*(f /. i)*>)) + ( Sum <*(f /. j)*>)) + ( Sum ((f /^ i) | ((j -' i) -' 1)))) + ( Sum (f /^ j))) by RLVECT_1:def 3

            .= (((( Sum ((f | (i -' 1)) ^ <*(f /. i)*>)) + ( Sum <*(f /. j)*>)) + ( Sum ((f /^ i) | ((j -' i) -' 1)))) + ( Sum (f /^ j))) by RLVECT_1: 41

            .= (((( Sum ((f | (i -' 1)) ^ <*(f /. i)*>)) + ( Sum ((f /^ i) | ((j -' i) -' 1)))) + ( Sum <*(f /. j)*>)) + ( Sum (f /^ j))) by RLVECT_1:def 3

            .= ((( Sum (((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1)))) + ( Sum <*(f /. j)*>)) + ( Sum (f /^ j))) by RLVECT_1: 41

            .= (( Sum ((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>)) + ( Sum (f /^ j))) by RLVECT_1: 41

            .= ( Sum (((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>) ^ (f /^ j))) by RLVECT_1: 41;

            (((((f | (i -' 1)) ^ <*(f /. i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>) ^ (f /^ j)) = (((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. j)*>) ^ (f /^ j)) by A3, PARTFUN1:def 6

            .= (((((f | (i -' 1)) ^ <*(f . i)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f . j)*>) ^ (f /^ j)) by A2, PARTFUN1:def 6

            .= f by A1, A4, FINSEQ_7: 1;

            hence thesis by A5;

          end;

            case

             A6: i > j;

            then ( Swap (f,j,i)) = (((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>) ^ (f /^ i)) by A1, FINSEQ_7: 27;

            

            then

             A7: ( Sum ( Swap (f,j,i))) = (( Sum ((((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. j)*>)) + ( Sum (f /^ i))) by RLVECT_1: 41

            .= ((( Sum (((f | (j -' 1)) ^ <*(f /. i)*>) ^ ((f /^ j) | ((i -' j) -' 1)))) + ( Sum <*(f /. j)*>)) + ( Sum (f /^ i))) by RLVECT_1: 41

            .= (((( Sum ((f | (j -' 1)) ^ <*(f /. i)*>)) + ( Sum ((f /^ j) | ((i -' j) -' 1)))) + ( Sum <*(f /. j)*>)) + ( Sum (f /^ i))) by RLVECT_1: 41

            .= ((((( Sum (f | (j -' 1))) + ( Sum <*(f /. i)*>)) + ( Sum ((f /^ j) | ((i -' j) -' 1)))) + ( Sum <*(f /. j)*>)) + ( Sum (f /^ i))) by RLVECT_1: 41

            .= ((((( Sum (f | (j -' 1))) + ( Sum <*(f /. i)*>)) + ( Sum <*(f /. j)*>)) + ( Sum ((f /^ j) | ((i -' j) -' 1)))) + ( Sum (f /^ i))) by RLVECT_1:def 3

            .= ((((( Sum (f | (j -' 1))) + ( Sum <*(f /. j)*>)) + ( Sum <*(f /. i)*>)) + ( Sum ((f /^ j) | ((i -' j) -' 1)))) + ( Sum (f /^ i))) by RLVECT_1:def 3

            .= (((( Sum ((f | (j -' 1)) ^ <*(f /. j)*>)) + ( Sum <*(f /. i)*>)) + ( Sum ((f /^ j) | ((i -' j) -' 1)))) + ( Sum (f /^ i))) by RLVECT_1: 41

            .= (((( Sum ((f | (j -' 1)) ^ <*(f /. j)*>)) + ( Sum ((f /^ j) | ((i -' j) -' 1)))) + ( Sum <*(f /. i)*>)) + ( Sum (f /^ i))) by RLVECT_1:def 3

            .= ((( Sum (((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1)))) + ( Sum <*(f /. i)*>)) + ( Sum (f /^ i))) by RLVECT_1: 41

            .= (( Sum ((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>)) + ( Sum (f /^ i))) by RLVECT_1: 41

            .= ( Sum (((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>) ^ (f /^ i))) by RLVECT_1: 41;

            (((((f | (j -' 1)) ^ <*(f /. j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>) ^ (f /^ i)) = (((((f | (j -' 1)) ^ <*(f . j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f /. i)*>) ^ (f /^ i)) by A2, PARTFUN1:def 6

            .= (((((f | (j -' 1)) ^ <*(f . j)*>) ^ ((f /^ j) | ((i -' j) -' 1))) ^ <*(f . i)*>) ^ (f /^ i)) by A3, PARTFUN1:def 6

            .= f by A1, A6, FINSEQ_7: 1;

            hence thesis by A7, FINSEQ_7: 21;

          end;

        end;

        hence thesis;

      end;

    end;

    definition

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

      assume

       A1: b2 divides b1;

      :: GROEB_2:def1

      func b1 / b2 -> bag of X means

      : Def1: (b2 + it ) = b1;

      existence by A1, TERMORD: 1;

      uniqueness

      proof

        let b3,b4 be bag of X;

        assume

         A2: (b2 + b3) = b1;

        assume

         A3: (b2 + b4) = b1;

         A4:

        now

          let x be object;

          assume x in ( dom b3);

          

          thus (b3 . x) = (((b2 . x) + (b3 . x)) -' (b2 . x)) by NAT_D: 34

          .= ((b1 . x) -' (b2 . x)) by A2, PRE_POLY:def 5

          .= (((b2 . x) + (b4 . x)) -' (b2 . x)) by A3, PRE_POLY:def 5

          .= (b4 . x) by NAT_D: 34;

        end;

        ( dom b3) = X by PARTFUN1:def 2

        .= ( dom b4) by PARTFUN1:def 2;

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    definition

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

      :: GROEB_2:def2

      func lcm (b1,b2) -> bag of X means

      : Def2: for k be object holds (it . k) = ( max ((b1 . k),(b2 . k)));

      existence

      proof

        defpred Q[ object, object] means $2 = ( max ((b1 . $1),(b2 . $1)));

        

         A1: for x be object st x in X holds ex y be object st Q[x, y];

        consider b be Function such that

         A2: ( dom b) = X & for x be object st x in X holds Q[x, (b . x)] from CLASSES1:sch 1( A1);

        reconsider b as ManySortedSet of X by A2, PARTFUN1:def 2, RELAT_1:def 18;

        now

          let u be object;

          assume u in ( rng b);

          then

          consider x be object such that

           A3: x in ( dom b) & u = (b . x) by FUNCT_1:def 3;

          u = ( max ((b1 . x),(b2 . x))) by A2, A3;

          hence u in NAT by ORDINAL1:def 12;

        end;

        then

         A4: ( rng b) c= NAT by TARSKI:def 3;

        now

          let u be object;

          

           A5: ( support b) c= ( dom b) by PRE_POLY: 37;

          assume

           A6: u in ( support b);

          then

           A7: (b . u) <> 0 by PRE_POLY:def 7;

          now

            assume

             A8: not u in (( support b1) \/ ( support b2));

            then not u in ( support b2) by XBOOLE_0:def 3;

            then

             A9: (b2 . u) = 0 by PRE_POLY:def 7;

             not u in ( support b1) by A8, XBOOLE_0:def 3;

            then (b1 . u) = 0 by PRE_POLY:def 7;

            then ( max ((b1 . u),(b2 . u))) = 0 by A9;

            hence contradiction by A2, A6, A7, A5;

          end;

          hence u in (( support b1) \/ ( support b2));

        end;

        then ( support b) c= (( support b1) \/ ( support b2)) by TARSKI:def 3;

        then

        reconsider b as bag of X by A4, PRE_POLY:def 8, VALUED_0:def 6;

        

         A10: ( dom b) = X by PARTFUN1:def 2

        .= ( dom b2) by PARTFUN1:def 2;

        take b;

        

         A11: ( dom b) = X by PARTFUN1:def 2

        .= ( dom b1) by PARTFUN1:def 2;

        now

          let k be object;

          now

            per cases ;

              case k in ( dom b);

              hence (b . k) = ( max ((b1 . k),(b2 . k))) by A2;

            end;

              case

               A12: not k in ( dom b);

              then (b1 . k) = 0 & (b2 . k) = 0 by A11, A10, FUNCT_1:def 2;

              hence (b . k) = ( max ((b1 . k),(b2 . k))) by A12, FUNCT_1:def 2;

            end;

          end;

          hence (b . k) = ( max ((b1 . k),(b2 . k)));

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let b3,b4 be bag of X;

        assume

         A13: for k be object holds (b3 . k) = ( max ((b1 . k),(b2 . k)));

        assume

         A14: for k be object holds (b4 . k) = ( max ((b1 . k),(b2 . k)));

         A15:

        now

          let u be object;

          assume u in ( dom b3);

          

          thus (b3 . u) = ( max ((b1 . u),(b2 . u))) by A13

          .= (b4 . u) by A14;

        end;

        ( dom b3) = X by PARTFUN1:def 2

        .= ( dom b4) by PARTFUN1:def 2;

        hence thesis by A15, FUNCT_1: 2;

      end;

      commutativity ;

      idempotence ;

    end

    notation

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

      synonym b1 lcm b2 for lcm (b1,b2);

    end

    definition

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

      :: GROEB_2:def3

      pred b1,b2 are_disjoint means for i be object holds (b1 . i) = 0 or (b2 . i) = 0 ;

    end

    notation

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

      antonym b1,b2 are_non_disjoint for b1,b2 are_disjoint ;

    end

    theorem :: GROEB_2:3

    

     Th3: for X be set, b1,b2 be bag of X holds b1 divides ( lcm (b1,b2)) & b2 divides ( lcm (b1,b2))

    proof

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

      set bb = ( lcm (b1,b2));

      now

        let k be object;

        (b1 . k) <= ( max ((b1 . k),(b2 . k))) by XXREAL_0: 25;

        hence (b1 . k) <= (bb . k) by Def2;

      end;

      hence b1 divides ( lcm (b1,b2)) by PRE_POLY:def 11;

      now

        let k be object;

        (b2 . k) <= ( max ((b1 . k),(b2 . k))) by XXREAL_0: 25;

        hence (b2 . k) <= (bb . k) by Def2;

      end;

      hence thesis by PRE_POLY:def 11;

    end;

    theorem :: GROEB_2:4

    

     Th4: for X be set, b1,b2,b3 be bag of X holds b1 divides b3 & b2 divides b3 implies ( lcm (b1,b2)) divides b3

    proof

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

      assume that

       A1: b1 divides b3 and

       A2: b2 divides b3;

      now

        let k be object;

        assume k in X;

        now

          per cases by XXREAL_0: 16;

            case ( max ((b1 . k),(b2 . k))) = (b1 . k);

            hence ( max ((b1 . k),(b2 . k))) <= (b3 . k) by A1, PRE_POLY:def 11;

          end;

            case ( max ((b1 . k),(b2 . k))) = (b2 . k);

            hence ( max ((b1 . k),(b2 . k))) <= (b3 . k) by A2, PRE_POLY:def 11;

          end;

        end;

        hence (( lcm (b1,b2)) . k) <= (b3 . k) by Def2;

      end;

      hence thesis by PRE_POLY: 46;

    end;

    theorem :: GROEB_2:5

    for X be set, b1,b2 be bag of X holds (b1,b2) are_disjoint iff ( lcm (b1,b2)) = (b1 + b2)

    proof

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

       A1:

      now

        assume

         A2: ( lcm (b1,b2)) = (b1 + b2);

        now

          let k be object;

          

           A3: (( lcm (b1,b2)) . k) = ( max ((b1 . k),(b2 . k))) by Def2;

          now

            per cases by A2, A3, XXREAL_0: 16;

              case ((b1 + b2) . k) = (b1 . k);

              then ((b1 . k) + (b2 . k)) = ((b1 . k) + 0 ) by PRE_POLY:def 5;

              hence (b2 . k) = 0 ;

            end;

              case ((b1 + b2) . k) = (b2 . k);

              then ((b1 . k) + (b2 . k)) = ( 0 + (b2 . k)) by PRE_POLY:def 5;

              hence (b1 . k) = 0 ;

            end;

          end;

          hence (b1 . k) = 0 or (b2 . k) = 0 ;

        end;

        hence (b1,b2) are_disjoint ;

      end;

      now

        assume

         A4: (b1,b2) are_disjoint ;

        now

          let k be object;

          now

            per cases by A4;

              case

               A5: (b1 . k) = 0 ;

              

              hence ((b1 + b2) . k) = ( 0 + (b2 . k)) by PRE_POLY:def 5

              .= ( max ((b1 . k),(b2 . k))) by A5, XXREAL_0:def 10;

            end;

              case

               A6: (b2 . k) = 0 ;

              

              hence ((b1 + b2) . k) = ((b1 . k) + 0 ) by PRE_POLY:def 5

              .= ( max ((b1 . k),(b2 . k))) by A6, XXREAL_0:def 10;

            end;

          end;

          hence ((b1 + b2) . k) = ( max ((b1 . k),(b2 . k)));

        end;

        hence ( lcm (b1,b2)) = (b1 + b2) by Def2;

      end;

      hence thesis by A1;

    end;

    theorem :: GROEB_2:6

    

     Th6: for X be set, b be bag of X holds (b / b) = ( EmptyBag X)

    proof

      let X be set, b be bag of X;

      (b + ( EmptyBag X)) = b by PRE_POLY: 53;

      hence thesis by Def1;

    end;

    theorem :: GROEB_2:7

    

     Th7: for X be set, b1,b2 be bag of X holds b2 divides b1 iff ( lcm (b1,b2)) = b1

    proof

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

      now

        assume

         A1: b2 divides b1;

        for k be object holds (b1 . k) = ( max ((b1 . k),(b2 . k))) by XXREAL_0:def 10, A1, PRE_POLY:def 11;

        hence ( lcm (b1,b2)) = b1 by Def2;

      end;

      hence thesis by Th3;

    end;

    theorem :: GROEB_2:8

    for X be set, b1,b2,b3 be bag of X holds b1 divides ( lcm (b2,b3)) implies ( lcm (b2,b1)) divides ( lcm (b2,b3))

    proof

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

      assume

       A1: b1 divides ( lcm (b2,b3));

      for k be object st k in X holds (( lcm (b2,b1)) . k) <= (( lcm (b2,b3)) . k)

      proof

        let k be object;

        assume k in X;

        (b1 . k) <= (( lcm (b2,b3)) . k) by A1, PRE_POLY:def 11;

        then

         A2: (b1 . k) <= ( max ((b2 . k),(b3 . k))) by Def2;

        (b2 . k) <= ( max ((b2 . k),(b3 . k))) by XXREAL_0: 25;

        then ( max ((b2 . k),(b1 . k))) <= ( max ((b2 . k),(b3 . k))) by A2, XXREAL_0: 28;

        then ( max ((b2 . k),(b1 . k))) <= (( lcm (b2,b3)) . k) by Def2;

        hence thesis by Def2;

      end;

      hence thesis by PRE_POLY: 46;

    end;

    theorem :: GROEB_2:9

    for X be set, b1,b2,b3 be bag of X holds ( lcm (b2,b1)) divides ( lcm (b2,b3)) implies ( lcm (b1,b3)) divides ( lcm (b2,b3))

    proof

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

      assume

       A1: ( lcm (b2,b1)) divides ( lcm (b2,b3));

      for k be object st k in X holds (( lcm (b1,b3)) . k) <= (( lcm (b2,b3)) . k)

      proof

        let k be object;

        assume k in X;

        

         A2: (b3 . k) <= ( max ((b2 . k),(b3 . k))) by XXREAL_0: 25;

        (( lcm (b2,b1)) . k) <= (( lcm (b2,b3)) . k) by A1, PRE_POLY:def 11;

        then ( max ((b2 . k),(b1 . k))) <= (( lcm (b2,b3)) . k) by Def2;

        then

         A3: ( max ((b2 . k),(b1 . k))) <= ( max ((b2 . k),(b3 . k))) by Def2;

        (b1 . k) <= ( max ((b2 . k),(b1 . k))) by XXREAL_0: 25;

        then (b1 . k) <= ( max ((b2 . k),(b3 . k))) by A3, XXREAL_0: 2;

        then ( max ((b1 . k),(b3 . k))) <= ( max ((b2 . k),(b3 . k))) by A2, XXREAL_0: 28;

        then ( max ((b1 . k),(b3 . k))) <= (( lcm (b2,b3)) . k) by Def2;

        hence thesis by Def2;

      end;

      hence thesis by PRE_POLY: 46;

    end;

    theorem :: GROEB_2:10

    for n be set, b1,b2,b3 be bag of n holds ( lcm (b1,b3)) divides ( lcm (b2,b3)) implies b1 divides ( lcm (b2,b3))

    proof

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

      assume

       A1: ( lcm (b1,b3)) divides ( lcm (b2,b3));

      for k be object st k in X holds (b1 . k) <= (( lcm (b2,b3)) . k)

      proof

        let k be object;

        assume k in X;

        (( lcm (b1,b3)) . k) <= (( lcm (b2,b3)) . k) by A1, PRE_POLY:def 11;

        then ( max ((b1 . k),(b3 . k))) <= (( lcm (b2,b3)) . k) by Def2;

        then

         A2: ( max ((b1 . k),(b3 . k))) <= ( max ((b2 . k),(b3 . k))) by Def2;

        (b1 . k) <= ( max ((b1 . k),(b3 . k))) by XXREAL_0: 25;

        then (b1 . k) <= ( max ((b2 . k),(b3 . k))) by A2, XXREAL_0: 2;

        hence thesis by Def2;

      end;

      hence thesis by PRE_POLY: 46;

    end;

    theorem :: GROEB_2:11

    for n be Element of NAT , T be connected admissible TermOrder of n, P be non empty Subset of ( Bags n) holds ex b be bag of n st b in P & for b9 be bag of n st b9 in P holds b <= (b9,T)

    proof

      let n be Element of NAT , T be connected admissible TermOrder of n, P be non empty Subset of ( Bags n);

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

      

       A1: T is_connected_in ( field T) by RELAT_2:def 14;

      reconsider b = m as bag of n;

      

       A2: m is_minimal_wrt (P,the InternalRel of R) by BAGORDER:def 17;

       A3:

      now

        let b9 be bag of n;

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

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

        then

         A4: b in ( field T) by RELAT_1: 15;

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

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

        then

         A5: b9 in ( field T) by RELAT_1: 15;

        assume

         A6: b9 in P;

        now

          per cases ;

            case b9 = b;

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

          end;

            case

             A7: b9 <> b;

            then not [b9, b] in T by A2, A6, WAYBEL_4:def 25;

            then [b, b9] in T by A1, A4, A5, A7, RELAT_2:def 6;

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

          end;

        end;

        hence b <= (b9,T);

      end;

      m in P by BAGORDER:def 17;

      hence thesis by A3;

    end;

    registration

      let L be add-associative right_zeroed right_complementable non trivial addLoopStr, a be non zero Element of L;

      cluster ( - a) -> non zero;

      coherence

      proof

        now

          assume ( - a) = ( 0. L);

          then ( - ( - a)) = ( 0. L) by RLVECT_1: 12;

          hence contradiction by RLVECT_1: 17;

        end;

        hence thesis;

      end;

    end

    registration

      let X be set, L be left_zeroed right_zeroed add-cancelable distributive non empty doubleLoopStr, m be Monomial of X, L, a be Element of L;

      cluster (a * m) -> monomial-like;

      coherence

      proof

        set p = (a * m);

        now

          per cases by POLYNOM7: 6;

            case

             A1: ( Support m) = {} ;

            now

              set b = the Element of ( Support p);

              assume

               A2: ( Support p) <> {} ;

              then b in ( Support p);

              then

              reconsider b as Element of ( Bags X);

              (p . b) = (a * (m . b)) by POLYNOM7:def 9

              .= (a * ( 0. L)) by A1, POLYNOM1:def 4

              .= ( 0. L) by BINOM: 2;

              hence contradiction by A2, POLYNOM1:def 4;

            end;

            hence thesis by POLYNOM7: 6;

          end;

            case ex b be bag of X st ( Support m) = {b};

            then

            consider b be bag of X such that

             A3: ( Support m) = {b};

            reconsider b as Element of ( Bags X) by PRE_POLY:def 12;

            now

              per cases ;

                case

                 A4: a = ( 0. L);

                now

                  set b = the Element of ( Support p);

                  assume

                   A5: ( Support p) <> {} ;

                  then b in ( Support p);

                  then

                  reconsider b as Element of ( Bags X);

                  (p . b) = (a * (m . b)) by POLYNOM7:def 9

                  .= ( 0. L) by A4, BINOM: 1;

                  hence contradiction by A5, POLYNOM1:def 4;

                end;

                hence ( Support p) = {} ;

              end;

                case a <> ( 0. L);

                 A6:

                now

                  let b9 be Element of ( Bags X);

                  assume b9 <> b;

                  then not b9 in ( Support m) by A3, TARSKI:def 1;

                  then

                   A7: (m . b9) = ( 0. L) by POLYNOM1:def 4;

                  (p . b9) = (a * (m . b9)) by POLYNOM7:def 9;

                  hence (p . b9) = ( 0. L) by A7, BINOM: 2;

                end;

                now

                  per cases ;

                    case

                     A8: (a * (m . b)) = ( 0. L);

                    now

                      set b9 = the Element of ( Support p);

                      assume

                       A9: ( Support p) <> {} ;

                      then b9 in ( Support p);

                      then

                      reconsider b9 as Element of ( Bags X);

                      

                       A10: (p . b9) <> ( 0. L) by A9, POLYNOM1:def 4;

                      then b9 = b by A6;

                      hence contradiction by A8, A10, POLYNOM7:def 9;

                    end;

                    hence ( Support p) = {} ;

                  end;

                    case

                     A11: (a * (m . b)) <> ( 0. L);

                     A12:

                    now

                      let u be object;

                      assume

                       A13: u in ( Support p);

                      then

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

                      (p . u9) <> ( 0. L) by A13, POLYNOM1:def 4;

                      then u9 = b by A6;

                      hence u in {b} by TARSKI:def 1;

                    end;

                    now

                      let u be object;

                      assume u in {b};

                      then

                       A14: u = b by TARSKI:def 1;

                      (p . b) <> ( 0. L) by A11, POLYNOM7:def 9;

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

                    end;

                    hence ( Support p) = {b} by A12, TARSKI: 2;

                  end;

                end;

                hence thesis by POLYNOM7: 6;

              end;

            end;

            hence thesis by POLYNOM7: 6;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let n be Ordinal, L be left_zeroed right_zeroed add-cancelable distributive domRing-like non trivial doubleLoopStr, p be non-zero Polynomial of n, L, a be non zero Element of L;

      cluster (a * p) -> non-zero;

      coherence

      proof

        set b = the Element of ( Support p);

        set ap = (a * p);

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

        then

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

        then b in ( Support p);

        then

        reconsider b as Element of ( Bags n);

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

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

        then (ap . b) <> ( 0. L) by POLYNOM7:def 9;

        then b in ( Support ap) by POLYNOM1:def 4;

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

        hence thesis by POLYNOM7:def 1;

      end;

    end

    theorem :: GROEB_2:12

    

     Th12: for n be Ordinal, L be right_zeroed right-distributive non empty doubleLoopStr, p,q be Series of n, L, b be bag of n holds (b *' (p + q)) = ((b *' p) + (b *' q))

    proof

      let n be Ordinal, L be right_zeroed right-distributive non empty doubleLoopStr, p1,p2 be Series of n, L, b be bag of n;

      set q1 = (b *' (p1 + p2)), q2 = ((b *' p1) + (b *' p2));

       A1:

      now

        let x be object;

        assume x in ( dom q1);

        then

        reconsider u = x as bag of n;

        now

          per cases ;

            case

             A2: b divides u;

            

            hence (q1 . u) = ((p1 + p2) . (u -' b)) by POLYRED:def 1

            .= ((p1 . (u -' b)) + (p2 . (u -' b))) by POLYNOM1: 15

            .= (((b *' p1) . u) + (p2 . (u -' b))) by A2, POLYRED:def 1

            .= (((b *' p1) . u) + ((b *' p2) . u)) by A2, POLYRED:def 1

            .= (q2 . u) by POLYNOM1: 15;

          end;

            case

             A3: not b divides u;

            

            hence (q1 . u) = ( 0. L) by POLYRED:def 1

            .= (( 0. L) + ( 0. L)) by RLVECT_1:def 4

            .= (((b *' p1) . u) + ( 0. L)) by A3, POLYRED:def 1

            .= (((b *' p1) . u) + ((b *' p2) . u)) by A3, POLYRED:def 1

            .= (q2 . u) by POLYNOM1: 15;

          end;

        end;

        hence (q1 . x) = (q2 . x);

      end;

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

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

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: GROEB_2:13

    

     Th13: for n be Ordinal, L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Series of n, L, b be bag of n holds (b *' ( - p)) = ( - (b *' p))

    proof

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

      set q1 = (b *' ( - p)), q2 = ( - (b *' p));

       A1:

      now

        let x be object;

        assume x in ( dom q1);

        then

        reconsider u = x as bag of n;

        now

          per cases ;

            case

             A2: b divides u;

            then

             A3: ((b *' p) . u) = (p . (u -' b)) by POLYRED:def 1;

            

            thus (q1 . u) = (( - p) . (u -' b)) by A2, POLYRED:def 1

            .= ( - (p . (u -' b))) by POLYNOM1: 17

            .= (( - (b *' p)) . u) by A3, POLYNOM1: 17;

          end;

            case

             A4: not b divides u;

            then

             A5: ((b *' p) . u) = ( 0. L) by POLYRED:def 1;

            

            thus (q1 . u) = ( 0. L) by A4, POLYRED:def 1

            .= ( - ( 0. L)) by RLVECT_1: 12

            .= (q2 . u) by A5, POLYNOM1: 17;

          end;

        end;

        hence (q1 . x) = (q2 . x);

      end;

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

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

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: GROEB_2:14

    

     Th14: for n be Ordinal, L be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, p be Series of n, L, b be bag of n, a be Element of L holds (b *' (a * p)) = (a * (b *' p))

    proof

      let n be Ordinal, L be left_zeroed right_add-cancelable right-distributive non empty doubleLoopStr, p be Series of n, L, b be bag of n, a be Element of L;

      set q1 = (b *' (a * p)), q2 = (a * (b *' p));

       A1:

      now

        let x be object;

        assume x in ( dom q1);

        then

        reconsider u = x as bag of n;

        now

          per cases ;

            case

             A2: b divides u;

            

            hence (q1 . u) = ((a * p) . (u -' b)) by POLYRED:def 1

            .= (a * (p . (u -' b))) by POLYNOM7:def 9

            .= (a * ((b *' p) . u)) by A2, POLYRED:def 1

            .= (q2 . u) by POLYNOM7:def 9;

          end;

            case

             A3: not b divides u;

            

            hence (q1 . u) = ( 0. L) by POLYRED:def 1

            .= (a * ( 0. L)) by BINOM: 2

            .= (a * ((b *' p) . u)) by A3, POLYRED:def 1

            .= (q2 . u) by POLYNOM7:def 9;

          end;

        end;

        hence (q1 . x) = (q2 . x);

      end;

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

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

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: GROEB_2:15

    

     Th15: for n be Ordinal, L be right-distributive non empty doubleLoopStr, p,q be Series of n, L, a be Element of L holds (a * (p + q)) = ((a * p) + (a * q))

    proof

      let n be Ordinal, L be right-distributive non empty doubleLoopStr, p1,p2 be Series of n, L, b be Element of L;

      set q1 = (b * (p1 + p2)), q2 = ((b * p1) + (b * p2));

       A1:

      now

        let x be object;

        assume x in ( dom q1);

        then

        reconsider u = x as bag of n;

        (q1 . u) = (b * ((p1 + p2) . u)) by POLYNOM7:def 9

        .= (b * ((p1 . u) + (p2 . u))) by POLYNOM1: 15

        .= ((b * (p1 . u)) + (b * (p2 . u))) by VECTSP_1:def 2

        .= (((b * p1) . u) + (b * (p2 . u))) by POLYNOM7:def 9

        .= (((b * p1) . u) + ((b * p2) . u)) by POLYNOM7:def 9

        .= (((b * p1) + (b * p2)) . u) by POLYNOM1: 15;

        hence (q1 . x) = (q2 . x);

      end;

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

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

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: GROEB_2:16

    

     Th16: for X be set, L be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of L holds ( - (a | (X,L))) = (( - a) | (X,L))

    proof

      let n be set, L be add-associative right_zeroed right_complementable non empty doubleLoopStr, a be Element of L;

       A1:

      now

        let u be object;

        assume u in ( dom (( - a) | (n,L)));

        then

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

        now

          per cases ;

            case

             A2: u9 = ( EmptyBag n);

            

            hence ( - ((a | (n,L)) . u9)) = ( - a) by POLYNOM7: 18

            .= ((( - a) | (n,L)) . u9) by A2, POLYNOM7: 18;

          end;

            case

             A3: u9 <> ( EmptyBag n);

            ( - ( 0. L)) = ( 0. L) by RLVECT_1: 12;

            

            hence ( - ((a | (n,L)) . u9)) = ( 0. L) by A3, POLYNOM7: 18

            .= ((( - a) | (n,L)) . u9) by A3, POLYNOM7: 18;

          end;

        end;

        hence ((( - a) | (n,L)) . u) = (( - (a | (n,L))) . u) by POLYNOM1: 17;

      end;

      ( dom ( - (a | (n,L)))) = ( Bags n) by FUNCT_2:def 1

      .= ( dom (( - a) | (n,L))) by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1: 2;

    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;

      

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

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

      set h = (p . l);

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

      then (l + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

      then

       A4: (l + 1) in ( dom p) by FINSEQ_1:def 3;

      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 ( Seg ( len p)) by A5, FINSEQ_1: 1;

        then l in ( dom p) by FINSEQ_1:def 3;

        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;

    begin

    theorem :: GROEB_2:17

    

     Th17: 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, P be Subset of ( Polynom-Ring (n,L)) holds (for p1,p2 be Polynomial of n, L st p1 <> p2 & p1 in P & p2 in P holds for m1,m2 be Monomial of n, L st ( HM ((m1 *' p1),T)) = ( HM ((m2 *' p2),T)) holds ( PolyRedRel (P,T)) reduces (((m1 *' p1) - (m2 *' p2)),( 0_ (n,L)))) implies P is_Groebner_basis_wrt T

    proof

      let n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, P be Subset of ( Polynom-Ring (n,L));

      assume

       A1: for p1,p2 be Polynomial of n, L st p1 <> p2 & p1 in P & p2 in P holds for m1,m2 be Monomial of n, L st ( HM ((m1 *' p1),T)) = ( HM ((m2 *' p2),T)) holds ( PolyRedRel (P,T)) reduces (((m1 *' p1) - (m2 *' p2)),( 0_ (n,L)));

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

      

       A2: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      now

        let a,b,c be object;

        assume that

         A3: [a, b] in R and

         A4: [a, c] in R;

        consider f,f1 be object such that

         A5: f in ( NonZero ( Polynom-Ring (n,L))) and

         A6: f1 in the carrier of ( Polynom-Ring (n,L)) and

         A7: [a, b] = [f, f1] by A3, ZFMISC_1:def 2;

        

         A8: not f in {( 0_ (n,L))} by A2, A5, XBOOLE_0:def 5;

        reconsider f as Polynomial of n, L by A5, POLYNOM1:def 11;

        f <> ( 0_ (n,L)) by A8, TARSKI:def 1;

        then

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

        reconsider f1 as Polynomial of n, L by A6, POLYNOM1:def 11;

        f reduces_to (f1,P,T) by A3, A7, POLYRED:def 13;

        then

        consider g1 be Polynomial of n, L such that

         A9: g1 in P and

         A10: f reduces_to (f1,g1,T) by POLYRED:def 7;

        ex b1 be bag of n st f reduces_to (f1,g1,b1,T) by A10, POLYRED:def 6;

        then

         A11: g1 <> ( 0_ (n,L)) by POLYRED:def 5;

        consider f9,f2 be object such that f9 in ( NonZero ( Polynom-Ring (n,L))) and

         A12: f2 in the carrier of ( Polynom-Ring (n,L)) and

         A13: [a, c] = [f9, f2] by A4, ZFMISC_1:def 2;

        reconsider f2 as Polynomial of n, L by A12, POLYNOM1:def 11;

        

         A14: f2 = c by A13, XTUPLE_0: 1;

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

        consider m1 be Monomial of n, L such that

         A15: f1 = (f - (m1 *' g1)) and

         A16: not ( HT ((m1 *' g1),T)) in ( Support f1) and ( HT ((m1 *' g1),T)) <= (( HT (f,T)),T) by A10, GROEB_1: 2;

        

         A17: f9 = a by A13, XTUPLE_0: 1;

        

         A18: f9 = a by A13, XTUPLE_0: 1

        .= f by A7, XTUPLE_0: 1;

        then f reduces_to (f2,P,T) by A4, A13, POLYRED:def 13;

        then

        consider g2 be Polynomial of n, L such that

         A19: g2 in P and

         A20: f reduces_to (f2,g2,T) by POLYRED:def 7;

        ex b2 be bag of n st f reduces_to (f2,g2,b2,T) by A20, POLYRED:def 6;

        then

         A21: g2 <> ( 0_ (n,L)) by POLYRED:def 5;

        then

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

        consider m2 be Monomial of n, L such that

         A22: f2 = (f - (m2 *' g2)) and

         A23: not ( HT ((m2 *' g2),T)) in ( Support f2) and ( HT ((m2 *' g2),T)) <= (( HT (f,T)),T) by A20, GROEB_1: 2;

        set mg1 = (m1 *' g1), mg2 = (m2 *' g2);

        

         A24: f1 = b by A7, XTUPLE_0: 1;

        now

          per cases ;

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

            

            then f1 = (f - ( 0_ (n,L))) by A15, POLYRED: 5

            .= f by POLYRED: 4;

            then

             A25: R reduces (b,c) by A4, A18, A24, A17, REWRITE1: 15;

            R reduces (c,c) by REWRITE1: 12;

            hence (b,c) are_convergent_wrt R by A25, REWRITE1:def 7;

          end;

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

            

            then f2 = (f - ( 0_ (n,L))) by A22, POLYRED: 5

            .= f by POLYRED: 4;

            then

             A26: R reduces (c,b) by A3, A18, A14, A17, REWRITE1: 15;

            R reduces (b,b) by REWRITE1: 12;

            hence (b,c) are_convergent_wrt R by A26, REWRITE1:def 7;

          end;

            case m1 <> ( 0_ (n,L)) & m2 <> ( 0_ (n,L));

            then

            reconsider m1, m2 as non-zero Monomial of n, L by POLYNOM7:def 1;

            (( HT (m1,T)) + ( HT (g1,T))) in ( Support mg1) by TERMORD: 29;

            then

             A27: mg1 <> ( 0_ (n,L)) by POLYNOM7: 1;

            (( HT (m2,T)) + ( HT (g2,T))) in ( Support mg2) by TERMORD: 29;

            then

             A28: mg2 <> ( 0_ (n,L)) by POLYNOM7: 1;

            

             A29: ( HC (g2,T)) <> ( 0. L);

            

             A30: ( - ( - (m1 *' g1))) = (m1 *' g1) by POLYNOM1: 19;

            

             A31: (f2 - f1) = ((f + ( - (m2 *' g2))) - (f - (m1 *' g1))) by A15, A22, POLYNOM1:def 7

            .= ((f + ( - (m2 *' g2))) - (f + ( - (m1 *' g1)))) by POLYNOM1:def 7

            .= ((f + ( - (m2 *' g2))) + ( - (f + ( - (m1 *' g1))))) by POLYNOM1:def 7

            .= ((f + ( - (m2 *' g2))) + (( - f) + ( - ( - (m1 *' g1))))) by POLYRED: 1

            .= (f + (( - (m2 *' g2)) + (( - f) + (m1 *' g1)))) by A30, POLYNOM1: 21

            .= (f + (( - f) + (( - (m2 *' g2)) + (m1 *' g1)))) by POLYNOM1: 21

            .= ((f + ( - f)) + (( - (m2 *' g2)) + (m1 *' g1))) by POLYNOM1: 21

            .= (( 0_ (n,L)) + (( - (m2 *' g2)) + (m1 *' g1))) by POLYRED: 3

            .= ((m1 *' g1) + ( - (m2 *' g2))) by POLYRED: 2

            .= (mg1 - mg2) by POLYNOM1:def 7;

            

             A32: ( HC (g1,T)) <> ( 0. L);

            

             A33: ( - ( - mg1)) = mg1 by POLYNOM1: 19;

            ( PolyRedRel (P,T)) reduces ((f2 - f1),( 0_ (n,L)))

            proof

              now

                per cases ;

                  case (mg1 - mg2) = ( 0_ (n,L));

                  hence thesis by A31, REWRITE1: 12;

                end;

                  case

                   A34: (mg1 - mg2) <> ( 0_ (n,L));

                  now

                    per cases ;

                      case g1 = g2;

                      

                      then (f2 - f1) = ((m1 *' g1) + ( - (m2 *' g1))) by A31, POLYNOM1:def 7

                      .= ((g1 *' m1) + (( - m2) *' g1)) by POLYRED: 6

                      .= ((m1 + ( - m2)) *' g1) by POLYNOM1: 26;

                      hence thesis by A9, POLYRED: 45;

                    end;

                      case

                       A35: g1 <> g2;

                      now

                        per cases ;

                          case

                           A36: ( HT (mg1,T)) <> ( HT (mg2,T));

                          now

                            per cases ;

                              case ( HT (mg2,T)) < (( HT (mg1,T)),T);

                              then not ( HT (mg1,T)) <= (( HT (mg2,T)),T) by TERMORD: 5;

                              then not ( HT (mg1,T)) in ( Support mg2) by TERMORD:def 6;

                              then

                               A37: (mg2 . ( HT (mg1,T))) = ( 0. L) by POLYNOM1:def 4;

                              

                               A38: ((mg1 - mg2) . ( HT (mg1,T))) = ((mg1 + ( - mg2)) . ( HT (mg1,T))) by POLYNOM1:def 7

                              .= ((mg1 . ( HT (mg1,T))) + (( - mg2) . ( HT (mg1,T)))) by POLYNOM1: 15

                              .= ((mg1 . ( HT (mg1,T))) + ( - (mg2 . ( HT (mg1,T))))) by POLYNOM1: 17

                              .= ((mg1 . ( HT (mg1,T))) + ( 0. L)) by A37, RLVECT_1: 12

                              .= (mg1 . ( HT (mg1,T))) by RLVECT_1:def 4

                              .= ( HC (mg1,T)) by TERMORD:def 7;

                              then ((mg1 - mg2) . ( HT (mg1,T))) <> ( 0. L) by A27, TERMORD: 17;

                              then

                               A39: ( HT (mg1,T)) in ( Support (mg1 - mg2)) by POLYNOM1:def 4;

                              

                               A40: (( HT (m1,T)) + ( HT (g1,T))) = ( HT (mg1,T)) by TERMORD: 31;

                              ((mg1 - mg2) - ((((mg1 - mg2) . ( HT (mg1,T))) / ( HC (g1,T))) * (( HT (m1,T)) *' g1))) = ((mg1 - mg2) - (((( HC (m1,T)) * ( HC (g1,T))) / ( HC (g1,T))) * (( HT (m1,T)) *' g1))) by A38, TERMORD: 32

                              .= ((mg1 - mg2) - (((( HC (m1,T)) * ( HC (g1,T))) * (( HC (g1,T)) " )) * (( HT (m1,T)) *' g1)))

                              .= ((mg1 - mg2) - ((( HC (m1,T)) * (( HC (g1,T)) * (( HC (g1,T)) " ))) * (( HT (m1,T)) *' g1))) by GROUP_1:def 3

                              .= ((mg1 - mg2) - ((( HC (m1,T)) * ( 1. L)) * (( HT (m1,T)) *' g1))) by A32, VECTSP_1:def 10

                              .= ((mg1 - mg2) - (( HC (m1,T)) * (( HT (m1,T)) *' g1)))

                              .= ((mg1 - mg2) - (( Monom (( HC (m1,T)),( HT (m1,T)))) *' g1)) by POLYRED: 22

                              .= ((mg1 - mg2) - (( Monom (( coefficient m1),( HT (m1,T)))) *' g1)) by TERMORD: 23

                              .= ((mg1 - mg2) - (( Monom (( coefficient m1),( term m1))) *' g1)) by TERMORD: 23

                              .= ((mg1 - mg2) - mg1) by POLYNOM7: 11

                              .= ((mg1 + ( - mg2)) - mg1) by POLYNOM1:def 7

                              .= ((mg1 + ( - mg2)) + ( - mg1)) by POLYNOM1:def 7

                              .= ((mg1 + ( - mg1)) + ( - mg2)) by POLYNOM1: 21

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

                              .= ( - mg2) by POLYRED: 2;

                              then (mg1 - mg2) reduces_to (( - mg2),g1,( HT (mg1,T)),T) by A11, A34, A39, A40, POLYRED:def 5;

                              then (mg1 - mg2) reduces_to (( - mg2),g1,T) by POLYRED:def 6;

                              then (mg1 - mg2) reduces_to (( - mg2),P,T) by A9, POLYRED:def 7;

                              then [(mg1 - mg2), ( - mg2)] in R by POLYRED:def 13;

                              then

                               A41: R reduces ((mg1 - mg2),( - mg2)) by REWRITE1: 15;

                              R reduces ((( - m2) *' g2),( 0_ (n,L))) by A19, POLYRED: 45;

                              then R reduces (( - mg2),( 0_ (n,L))) by POLYRED: 6;

                              hence thesis by A31, A41, REWRITE1: 16;

                            end;

                              case not ( HT (mg2,T)) < (( HT (mg1,T)),T);

                              then ( HT (mg1,T)) <= (( HT (mg2,T)),T) by TERMORD: 5;

                              then ( HT (mg1,T)) < (( HT (mg2,T)),T) by A36, TERMORD:def 3;

                              then not ( HT (mg2,T)) <= (( HT (mg1,T)),T) by TERMORD: 5;

                              then not ( HT (mg2,T)) in ( Support mg1) by TERMORD:def 6;

                              then

                               A42: (mg1 . ( HT (mg2,T))) = ( 0. L) by POLYNOM1:def 4;

                              

                               A43: ((mg2 - mg1) . ( HT (mg2,T))) = ((mg2 + ( - mg1)) . ( HT (mg2,T))) by POLYNOM1:def 7

                              .= ((mg2 . ( HT (mg2,T))) + (( - mg1) . ( HT (mg2,T)))) by POLYNOM1: 15

                              .= ((mg2 . ( HT (mg2,T))) + ( - (mg1 . ( HT (mg2,T))))) by POLYNOM1: 17

                              .= ((mg2 . ( HT (mg2,T))) + ( 0. L)) by A42, RLVECT_1: 12

                              .= (mg2 . ( HT (mg2,T))) by RLVECT_1:def 4

                              .= ( HC (mg2,T)) by TERMORD:def 7;

                              then ((mg2 - mg1) . ( HT (mg2,T))) <> ( 0. L) by A28, TERMORD: 17;

                              then

                               A44: ( HT (mg2,T)) in ( Support (mg2 - mg1)) by POLYNOM1:def 4;

                              reconsider x = ( - ( 0_ (n,L))) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

                              

                               A45: (( HT (m2,T)) + ( HT (g2,T))) = ( HT (mg2,T)) by TERMORD: 31;

                              reconsider x as Element of ( Polynom-Ring (n,L));

                              ( 0. ( Polynom-Ring (n,L))) = ( 0_ (n,L)) by POLYNOM1:def 11;

                              

                              then

                               A46: (x + ( 0. ( Polynom-Ring (n,L)))) = (( - ( 0_ (n,L))) + ( 0_ (n,L))) by POLYNOM1:def 11

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

                              .= ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

                               A47:

                              now

                                assume (mg2 - mg1) = ( 0_ (n,L));

                                then ( - (mg2 + ( - mg1))) = ( - ( 0_ (n,L))) by POLYNOM1:def 7;

                                then (( - mg2) + ( - ( - mg1))) = ( - ( 0_ (n,L))) by POLYRED: 1;

                                

                                then (mg1 + ( - mg2)) = ( - ( 0. ( Polynom-Ring (n,L)))) by A33, A46, RLVECT_1: 6

                                .= ( 0. ( Polynom-Ring (n,L))) by RLVECT_1: 12

                                .= ( 0_ (n,L)) by POLYNOM1:def 11;

                                hence contradiction by A34, POLYNOM1:def 7;

                              end;

                              ((mg2 - mg1) - ((((mg2 - mg1) . ( HT (mg2,T))) / ( HC (g2,T))) * (( HT (m2,T)) *' g2))) = ((mg2 - mg1) - (((( HC (m2,T)) * ( HC (g2,T))) / ( HC (g2,T))) * (( HT (m2,T)) *' g2))) by A43, TERMORD: 32

                              .= ((mg2 - mg1) - (((( HC (m2,T)) * ( HC (g2,T))) * (( HC (g2,T)) " )) * (( HT (m2,T)) *' g2)))

                              .= ((mg2 - mg1) - ((( HC (m2,T)) * (( HC (g2,T)) * (( HC (g2,T)) " ))) * (( HT (m2,T)) *' g2))) by GROUP_1:def 3

                              .= ((mg2 - mg1) - ((( HC (m2,T)) * ( 1. L)) * (( HT (m2,T)) *' g2))) by A29, VECTSP_1:def 10

                              .= ((mg2 - mg1) - (( HC (m2,T)) * (( HT (m2,T)) *' g2)))

                              .= ((mg2 - mg1) - (( Monom (( HC (m2,T)),( HT (m2,T)))) *' g2)) by POLYRED: 22

                              .= ((mg2 - mg1) - (( Monom (( coefficient m2),( HT (m2,T)))) *' g2)) by TERMORD: 23

                              .= ((mg2 - mg1) - (( Monom (( coefficient m2),( term m2))) *' g2)) by TERMORD: 23

                              .= ((mg2 - mg1) - mg2) by POLYNOM7: 11

                              .= ((mg2 + ( - mg1)) - mg2) by POLYNOM1:def 7

                              .= ((mg2 + ( - mg1)) + ( - mg2)) by POLYNOM1:def 7

                              .= ((mg2 + ( - mg2)) + ( - mg1)) by POLYNOM1: 21

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

                              .= ( - mg1) by POLYRED: 2;

                              then (mg2 - mg1) reduces_to (( - mg1),g2,( HT (mg2,T)),T) by A21, A44, A45, A47, POLYRED:def 5;

                              then (mg2 - mg1) reduces_to (( - mg1),g2,T) by POLYRED:def 6;

                              then (mg2 - mg1) reduces_to (( - mg1),P,T) by A19, POLYRED:def 7;

                              then [(mg2 - mg1), ( - mg1)] in R by POLYRED:def 13;

                              then

                               A48: R reduces ((mg2 - mg1),( - mg1)) by REWRITE1: 15;

                              

                               A49: ( - ( 1_ (n,L))) = ( - (( 1. L) | (n,L))) by POLYNOM7: 20

                              .= (( - ( 1. L)) | (n,L)) by Th16;

                              R reduces ((( - m1) *' g1),( 0_ (n,L))) by A9, POLYRED: 45;

                              then R reduces (( - mg1),( 0_ (n,L))) by POLYRED: 6;

                              then R reduces ((mg2 - mg1),( 0_ (n,L))) by A48, REWRITE1: 16;

                              then

                               A50: R reduces ((( - ( 1_ (n,L))) *' (mg2 - mg1)),(( - ( 1_ (n,L))) *' ( 0_ (n,L)))) by A49, POLYRED: 47;

                              (( - ( 1_ (n,L))) *' (mg2 - mg1)) = (( - ( 1_ (n,L))) *' (mg2 + ( - mg1))) by POLYNOM1:def 7

                              .= ((( - ( 1_ (n,L))) *' mg2) + (( - ( 1_ (n,L))) *' ( - mg1))) by POLYNOM1: 26

                              .= (( - (( 1_ (n,L)) *' mg2)) + (( - ( 1_ (n,L))) *' ( - mg1))) by POLYRED: 6

                              .= ((( 1_ (n,L)) *' ( - mg2)) + (( - ( 1_ (n,L))) *' ( - mg1))) by POLYRED: 6

                              .= ((( 1_ (n,L)) *' ( - mg2)) + ( - (( 1_ (n,L)) *' ( - mg1)))) by POLYRED: 6

                              .= ((( 1_ (n,L)) *' ( - mg2)) + (( 1_ (n,L)) *' ( - ( - mg1)))) by POLYRED: 6

                              .= (( - mg2) + (( 1_ (n,L)) *' mg1)) by A33, POLYNOM1: 30

                              .= (mg1 + ( - mg2)) by POLYNOM1: 30

                              .= (mg1 - mg2) by POLYNOM1:def 7;

                              hence thesis by A31, A50, POLYNOM1: 28;

                            end;

                          end;

                          hence thesis;

                        end;

                          case

                           A51: ( HT (mg1,T)) = ( HT (mg2,T));

                          ((f - mg2) . ( HT (mg2,T))) = ( 0. L) by A22, A23, POLYNOM1:def 4;

                          then ((f + ( - mg2)) . ( HT (mg2,T))) = ( 0. L) by POLYNOM1:def 7;

                          then ((f . ( HT (mg2,T))) + (( - mg2) . ( HT (mg2,T)))) = ( 0. L) by POLYNOM1: 15;

                          then ((f . ( HT (mg2,T))) + ( - (mg2 . ( HT (mg2,T))))) = ( 0. L) by POLYNOM1: 17;

                          then

                           A52: (f . ( HT (mg2,T))) = ( - ( - (mg2 . ( HT (mg2,T))))) by RLVECT_1: 6;

                          ((f - mg1) . ( HT (mg1,T))) = ( 0. L) by A15, A16, POLYNOM1:def 4;

                          then ((f + ( - mg1)) . ( HT (mg1,T))) = ( 0. L) by POLYNOM1:def 7;

                          then ((f . ( HT (mg1,T))) + (( - mg1) . ( HT (mg1,T)))) = ( 0. L) by POLYNOM1: 15;

                          then ((f . ( HT (mg1,T))) + ( - (mg1 . ( HT (mg1,T))))) = ( 0. L) by POLYNOM1: 17;

                          then

                           A53: (f . ( HT (mg1,T))) = ( - ( - (mg1 . ( HT (mg1,T))))) by RLVECT_1: 6;

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

                          .= (f . ( HT (mg1,T))) by A53, RLVECT_1: 17

                          .= (mg2 . ( HT (mg2,T))) by A51, A52, RLVECT_1: 17

                          .= ( HC (mg2,T)) by TERMORD:def 7;

                          

                          then ( HM (mg1,T)) = ( Monom (( HC (mg2,T)),( HT (mg2,T)))) by A51, TERMORD:def 8

                          .= ( HM (mg2,T)) by TERMORD:def 8;

                          hence thesis by A1, A9, A19, A31, A35;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

            hence (b,c) are_convergent_wrt R by A24, A14, POLYRED: 50, REWRITE1: 40;

          end;

        end;

        hence (b,c) are_convergent_wrt R;

      end;

      then ( PolyRedRel (P,T)) is locally-confluent by REWRITE1:def 24;

      hence thesis by GROEB_1:def 3;

    end;

    definition

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L;

      :: GROEB_2:def4

      func S-Poly (p1,p2,T) -> Polynomial of n, L equals ((( HC (p2,T)) * ((( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))) *' p1)) - (( HC (p1,T)) * ((( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))) *' p2)));

      coherence ;

    end

    

     Lm2: for L be add-associative left_zeroed right_zeroed add-cancelable right_complementable associative distributive well-unital non empty doubleLoopStr, P be Subset of L, p be Element of L st p in P holds p in (P -Ideal )

    proof

      let L be add-associative left_zeroed right_zeroed add-cancelable associative distributive well-unital right_complementable non empty doubleLoopStr, P be Subset of L, p be Element of L;

      set f = <*p*>;

      assume

       A1: p in P;

      then

      reconsider P9 = P as non empty Subset of L;

      now

        let i be set;

        assume

         A2: i in ( dom f);

        ( dom f) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then i = 1 by A2, TARSKI:def 1;

        

        then (f /. i) = (f . 1) by A2, PARTFUN1:def 6

        .= p by FINSEQ_1: 40

        .= (( 1. L) * p)

        .= ((( 1. L) * p) * ( 1. L));

        hence ex u,v be Element of L, a be Element of P9 st (f /. i) = ((u * a) * v) by A1;

      end;

      then

      reconsider f as LinearCombination of P9 by IDEAL_1:def 8;

      ( Sum f) = p by RLVECT_1: 44;

      hence thesis by IDEAL_1: 60;

    end;

    

     Lm3: for n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, f,g be Element of ( Polynom-Ring (n,L)) holds (f = p & g = q) implies (f - g) = (p - q)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed well-unital distributive non trivial doubleLoopStr, p,q be Polynomial of n, L, f,g be Element of ( Polynom-Ring (n,L));

      assume that

       A1: f = p and

       A2: g = q;

      reconsider x = ( - q) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider x as Element of ( Polynom-Ring (n,L));

      (x + g) = (( - q) + q) by A2, POLYNOM1:def 11

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

      .= ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      then

       A3: ( - q) = ( - g) by RLVECT_1: 6;

      

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

      .= (f + ( - g)) by A1, A3, POLYNOM1:def 11

      .= (f - g);

    end;

    theorem :: GROEB_2:18

    

     Th18: 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 Abelian non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), p1,p2 be Polynomial of n, L st p1 in P & p2 in P holds ( S-Poly (p1,p2,T)) in (P -Ideal )

    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 Abelian non trivial doubleLoopStr, P be Subset of ( Polynom-Ring (n,L)), p1,p2 be Polynomial of n, L;

      assume that

       A1: p1 in P and

       A2: p2 in P;

      set q1 = ( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))), q2 = ( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T)))));

      reconsider p19 = p1, p29 = p2 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider p19, p29 as Element of ( Polynom-Ring (n,L));

      reconsider q19 = q1, q29 = q2 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider q19, q29 as Element of ( Polynom-Ring (n,L));

      p29 in (P -Ideal ) by A2, Lm2;

      then

       A3: (q29 * p29) in (P -Ideal ) by IDEAL_1:def 2;

      p19 in (P -Ideal ) by A1, Lm2;

      then (q19 * p19) in (P -Ideal ) by IDEAL_1:def 2;

      then

       A4: ((q19 * p19) - (q29 * p29)) in (P -Ideal ) by A3, IDEAL_1: 16;

      set q = ( S-Poly (p1,p2,T));

      

       A5: (q1 *' p1) = (q19 * p19) & (q2 *' p2) = (q29 * p29) by POLYNOM1:def 11;

      q = ((q1 *' p1) - (( HC (p1,T)) * ((( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))) *' p2))) by POLYRED: 22

      .= ((q1 *' p1) - (q2 *' p2)) by POLYRED: 22;

      hence thesis by A4, A5, Lm3;

    end;

    theorem :: GROEB_2:19

    

     Th19: 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, m1,m2 be Monomial of n, L holds ( S-Poly (m1,m2,T)) = ( 0_ (n,L))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, m1,m2 be Monomial of n, L;

      per cases ;

        suppose

         A1: m1 = ( 0_ (n,L));

        

         A2: ( HC (( Monom (( HC (( 0_ (n,L)),T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))))),T)) = ( coefficient ( Monom (( HC (( 0_ (n,L)),T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T)))))) by TERMORD: 23

        .= ( HC (( 0_ (n,L)),T)) by POLYNOM7: 9

        .= ( 0. L) by TERMORD: 17;

        

        thus ( S-Poly (m1,m2,T)) = ((( Monom (( HC (m2,T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))))) *' ( 0_ (n,L))) - (( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))) *' m2))) by A1, POLYRED: 22

        .= (( 0_ (n,L)) - (( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))) *' m2))) by POLYNOM1: 28

        .= (( 0_ (n,L)) - (( Monom (( HC (( 0_ (n,L)),T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))))) *' m2)) by POLYRED: 22

        .= (( 0_ (n,L)) - (( 0_ (n,L)) *' m2)) by A2, TERMORD: 17

        .= (( 0_ (n,L)) - ( 0_ (n,L))) by POLYRED: 5

        .= ( 0_ (n,L)) by POLYNOM1: 24;

      end;

        suppose

         A3: m2 = ( 0_ (n,L));

        

         A4: ( HC (( Monom (( HC (( 0_ (n,L)),T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))))),T)) = ( coefficient ( Monom (( HC (( 0_ (n,L)),T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T)))))) by TERMORD: 23

        .= ( HC (( 0_ (n,L)),T)) by POLYNOM7: 9

        .= ( 0. L) by TERMORD: 17;

        

        thus ( S-Poly (m1,m2,T)) = ((( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))) *' m1)) - (( Monom (( HC (m1,T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))))) *' ( 0_ (n,L)))) by A3, POLYRED: 22

        .= ((( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))) *' m1)) - ( 0_ (n,L))) by POLYNOM1: 28

        .= ((( Monom (( HC (( 0_ (n,L)),T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))))) *' m1) - ( 0_ (n,L))) by POLYRED: 22

        .= ((( 0_ (n,L)) *' m1) - ( 0_ (n,L))) by A4, TERMORD: 17

        .= (( 0_ (n,L)) - ( 0_ (n,L))) by POLYRED: 5

        .= ( 0_ (n,L)) by POLYNOM1: 24;

      end;

        suppose

         A5: m1 <> ( 0_ (n,L)) & m2 <> ( 0_ (n,L));

        then ( HC (m2,T)) <> ( 0. L) by TERMORD: 17;

        then

         A6: ( HC (m2,T)) is non zero;

        ( HC (m1,T)) <> ( 0. L) by A5, TERMORD: 17;

        then

         A7: ( HC (m1,T)) is non zero;

        

         A8: ( HT (m2,T)) divides ( lcm (( HT (m1,T)),( HT (m2,T)))) by Th3;

        

         A9: m2 = ( Monom (( coefficient m2),( term m2))) by POLYNOM7: 11

        .= ( Monom (( HC (m2,T)),( term m2))) by TERMORD: 23

        .= ( Monom (( HC (m2,T)),( HT (m2,T)))) by TERMORD: 23;

        

         A10: ( HT (m1,T)) divides ( lcm (( HT (m1,T)),( HT (m2,T)))) by Th3;

        

         A11: m1 = ( Monom (( coefficient m1),( term m1))) by POLYNOM7: 11

        .= ( Monom (( HC (m1,T)),( term m1))) by TERMORD: 23

        .= ( Monom (( HC (m1,T)),( HT (m1,T)))) by TERMORD: 23;

        

         A12: (( HC (m1,T)) * ((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))) *' m2)) = (( Monom (( HC (m1,T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))))) *' m2) by POLYRED: 22

        .= ( Monom ((( HC (m2,T)) * ( HC (m1,T))),((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m2,T))) + ( HT (m2,T))))) by A7, A6, A9, TERMORD: 3

        .= ( Monom ((( HC (m2,T)) * ( HC (m1,T))),( lcm (( HT (m1,T)),( HT (m2,T)))))) by A8, Def1;

        (( HC (m2,T)) * ((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))) *' m1)) = (( Monom (( HC (m2,T)),(( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))))) *' m1) by POLYRED: 22

        .= ( Monom ((( HC (m2,T)) * ( HC (m1,T))),((( lcm (( HT (m1,T)),( HT (m2,T)))) / ( HT (m1,T))) + ( HT (m1,T))))) by A7, A6, A11, TERMORD: 3

        .= ( Monom ((( HC (m2,T)) * ( HC (m1,T))),( lcm (( HT (m1,T)),( HT (m2,T)))))) by A10, Def1;

        hence thesis by A12, POLYNOM1: 24;

      end;

    end;

    theorem :: GROEB_2:20

    

     Th20: 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 Polynomial of n, L holds ( S-Poly (p,( 0_ (n,L)),T)) = ( 0_ (n,L)) & ( S-Poly (( 0_ (n,L)),p,T)) = ( 0_ (n,L))

    proof

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

      set p2 = ( 0_ (n,L));

      

      thus ( S-Poly (p,( 0_ (n,L)),T)) = ((( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (p,T)),( HT (p2,T)))) / ( HT (p,T))) *' p)) - (( Monom (( HC (p,T)),(( lcm (( HT (p,T)),( HT (p2,T)))) / ( HT (p2,T))))) *' ( 0_ (n,L)))) by POLYRED: 22

      .= ((( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (p,T)),( HT (p2,T)))) / ( HT (p,T))) *' p)) - ( 0_ (n,L))) by POLYNOM1: 28

      .= ((( 0. L) * ((( lcm (( HT (p,T)),( HT (p2,T)))) / ( HT (p,T))) *' p)) - ( 0_ (n,L))) by TERMORD: 17

      .= (((( 0. L) | (n,L)) *' ((( lcm (( HT (p,T)),( HT (p2,T)))) / ( HT (p,T))) *' p)) - ( 0_ (n,L))) by POLYNOM7: 27

      .= ((( 0_ (n,L)) *' ((( lcm (( HT (p,T)),( HT (p2,T)))) / ( HT (p,T))) *' p)) - ( 0_ (n,L))) by POLYNOM7: 19

      .= (( 0_ (n,L)) - ( 0_ (n,L))) by POLYRED: 5

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

      

      thus ( S-Poly (( 0_ (n,L)),p,T)) = ((( Monom (( HC (p,T)),(( lcm (( HT (p2,T)),( HT (p,T)))) / ( HT (p2,T))))) *' ( 0_ (n,L))) - (( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (p2,T)),( HT (p,T)))) / ( HT (p,T))) *' p))) by POLYRED: 22

      .= (( 0_ (n,L)) - (( HC (( 0_ (n,L)),T)) * ((( lcm (( HT (p2,T)),( HT (p,T)))) / ( HT (p,T))) *' p))) by POLYNOM1: 28

      .= (( 0_ (n,L)) - (( 0. L) * ((( lcm (( HT (p2,T)),( HT (p,T)))) / ( HT (p,T))) *' p))) by TERMORD: 17

      .= (( 0_ (n,L)) - ((( 0. L) | (n,L)) *' ((( lcm (( HT (p2,T)),( HT (p,T)))) / ( HT (p,T))) *' p))) by POLYNOM7: 27

      .= (( 0_ (n,L)) - (( 0_ (n,L)) *' ((( lcm (( HT (p2,T)),( HT (p,T)))) / ( HT (p,T))) *' p))) by POLYNOM7: 19

      .= (( 0_ (n,L)) - ( 0_ (n,L))) by POLYRED: 5

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

    end;

    theorem :: GROEB_2:21

    for n be Ordinal, T be admissible connected 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 holds ( S-Poly (p1,p2,T)) = ( 0_ (n,L)) or ( HT (( S-Poly (p1,p2,T)),T)) < (( lcm (( HT (p1,T)),( HT (p2,T)))),T)

    proof

      let n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non trivial doubleLoopStr, p1,p2 be Polynomial of n, L;

      assume

       A1: ( S-Poly (p1,p2,T)) <> ( 0_ (n,L));

      set sp = ( S-Poly (p1,p2,T)), g1 = (( HC (p2,T)) * ((( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))) *' p1)), g2 = (( HC (p1,T)) * ((( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))) *' p2));

      per cases ;

        suppose p1 = ( 0_ (n,L)) or p2 = ( 0_ (n,L));

        hence thesis by A1, Th20;

      end;

        suppose

         A2: p1 <> ( 0_ (n,L)) & p2 <> ( 0_ (n,L));

        then

         A3: ( HC (p2,T)) <> ( 0. L) by TERMORD: 17;

        then

         A4: ( HC (p2,T)) is non zero;

        

         A5: ( HT (( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))),T)) = ( term ( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T)))))) by TERMORD: 23

        .= (( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))) by A4, POLYNOM7: 10;

        

         A6: p1 is non-zero by A2, POLYNOM7:def 1;

        ( HC (( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))),T)) = ( coefficient ( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T)))))) by TERMORD: 23

        .= ( HC (p2,T)) by POLYNOM7: 9;

        then ( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))) <> ( 0_ (n,L)) by A3, TERMORD: 17;

        then

         A7: ( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))) is non-zero by POLYNOM7:def 1;

        

         A8: ( HC (g1,T)) = ( HC ((( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))) *' p1),T)) by POLYRED: 22

        .= (( HC (( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))),T)) * ( HC (p1,T))) by A6, A7, TERMORD: 32

        .= (( coefficient ( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T)))))) * ( HC (p1,T))) by TERMORD: 23

        .= (( HC (p1,T)) * ( HC (p2,T))) by POLYNOM7: 9;

        

         A9: ( HT (p1,T)) divides ( lcm (( HT (p1,T)),( HT (p2,T)))) by Th3;

        

         A10: ( HT (g1,T)) = ( HT ((( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))) *' p1),T)) by POLYRED: 22

        .= (( HT (( Monom (( HC (p2,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p1,T))))),T)) + ( HT (p1,T))) by A6, A7, TERMORD: 31

        .= ( lcm (( HT (p1,T)),( HT (p2,T)))) by A9, A5, Def1;

        

         A11: ( HC (p1,T)) <> ( 0. L) by A2, TERMORD: 17;

        then

         A12: ( HC (p1,T)) is non zero;

        

         A13: ( HT (( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))),T)) = ( term ( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T)))))) by TERMORD: 23

        .= (( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))) by A12, POLYNOM7: 10;

        

         A14: p2 is non-zero by A2, POLYNOM7:def 1;

        ( HC (( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))),T)) = ( coefficient ( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T)))))) by TERMORD: 23

        .= ( HC (p1,T)) by POLYNOM7: 9;

        then ( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))) <> ( 0_ (n,L)) by A11, TERMORD: 17;

        then

         A15: ( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))) is non-zero by POLYNOM7:def 1;

        ( Support sp) <> {} by A1, POLYNOM7: 1;

        then

         A16: ( HT (sp,T)) in ( Support sp) by TERMORD:def 6;

        

         A17: ( HT (p2,T)) divides ( lcm (( HT (p1,T)),( HT (p2,T)))) by Th3;

        

         A18: ( HC (g2,T)) = ( HC ((( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))) *' p2),T)) by POLYRED: 22

        .= (( HC (( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))),T)) * ( HC (p2,T))) by A14, A15, TERMORD: 32

        .= (( coefficient ( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T)))))) * ( HC (p2,T))) by TERMORD: 23

        .= (( HC (p1,T)) * ( HC (p2,T))) by POLYNOM7: 9;

        

         A19: ( HT (g2,T)) = ( HT ((( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))) *' p2),T)) by POLYRED: 22

        .= (( HT (( Monom (( HC (p1,T)),(( lcm (( HT (p1,T)),( HT (p2,T)))) / ( HT (p2,T))))),T)) + ( HT (p2,T))) by A14, A15, TERMORD: 31

        .= ( lcm (( HT (p1,T)),( HT (p2,T)))) by A17, A13, Def1;

        

        then (sp . ( lcm (( HT (p1,T)),( HT (p2,T))))) = ((g1 + ( - g2)) . ( HT (g2,T))) by POLYNOM1:def 7

        .= ((g1 . ( HT (g2,T))) + (( - g2) . ( HT (g2,T)))) by POLYNOM1: 15

        .= ((g1 . ( HT (g2,T))) + ( - (g2 . ( HT (g2,T))))) by POLYNOM1: 17

        .= (( HC (g1,T)) + ( - (g2 . ( HT (g2,T))))) by A10, A19, TERMORD:def 7

        .= (( HC (g1,T)) + ( - ( HC (g2,T)))) by TERMORD:def 7

        .= ( 0. L) by A8, A18, RLVECT_1: 5;

        then

         A20: not ( lcm (( HT (p1,T)),( HT (p2,T)))) in ( Support sp) by POLYNOM1:def 4;

        ( HT (sp,T)) <= (( max (( HT (g1,T)),( HT (g2,T)),T)),T) by GROEB_1: 7;

        then ( HT (sp,T)) <= (( lcm (( HT (p1,T)),( HT (p2,T)))),T) by A10, A19, TERMORD: 12;

        hence thesis by A16, A20, TERMORD:def 3;

      end;

    end;

    theorem :: GROEB_2:22

    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, p1,p2 be non-zero Polynomial of n, L holds ( HT (p2,T)) divides ( HT (p1,T)) implies (( HC (p2,T)) * p1) top_reduces_to (( S-Poly (p1,p2,T)),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 almost_left_invertible non trivial doubleLoopStr, p1,p2 be non-zero Polynomial of n, L;

      set hcp2 = ( HC (p2,T));

      assume

       A1: ( HT (p2,T)) divides ( HT (p1,T));

      then

      consider b be bag of n such that

       A2: ( HT (p1,T)) = (( HT (p2,T)) + b) by TERMORD: 1;

      set g = ((hcp2 * p1) - ((((hcp2 * p1) . ( HT (p1,T))) / ( HC (p2,T))) * (b *' p2)));

      

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

      

       A4: hcp2 <> ( 0. L);

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

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

      then

       A5: ( HT (p1,T)) in ( Support p1) by TERMORD:def 6;

      

       A6: ( Support p1) c= ( Support (hcp2 * p1)) by POLYRED: 20;

      then (hcp2 * p1) <> ( 0_ (n,L)) by A5, POLYNOM7: 1;

      then

       A7: ( HT ((hcp2 * p1),T)) = ( HT (p1,T)) & (hcp2 * p1) reduces_to (g,p2,( HT (p1,T)),T) by A3, A5, A2, A6, POLYRED: 21, POLYRED:def 5;

      

       A8: ( lcm (( HT (p1,T)),( HT (p2,T)))) = ( HT (p1,T)) by A1, Th7;

      g = ((hcp2 * p1) - (((hcp2 * (p1 . ( HT (p1,T)))) / ( HC (p2,T))) * (b *' p2))) by POLYNOM7:def 9

      .= ((hcp2 * p1) - (((hcp2 * ( HC (p1,T))) / ( HC (p2,T))) * (b *' p2))) by TERMORD:def 7

      .= ((hcp2 * p1) - (((hcp2 * ( HC (p1,T))) * (( HC (p2,T)) " )) * (b *' p2)))

      .= ((hcp2 * p1) - ((( HC (p1,T)) * (hcp2 * (( HC (p2,T)) " ))) * (b *' p2))) by GROUP_1:def 3

      .= ((hcp2 * p1) - ((( HC (p1,T)) * ( 1. L)) * (b *' p2))) by A4, VECTSP_1:def 10

      .= ((hcp2 * p1) - (( HC (p1,T)) * (b *' p2)))

      .= ((( HC (p2,T)) * (( EmptyBag n) *' p1)) - (( HC (p1,T)) * (b *' p2))) by POLYRED: 17

      .= ((( HC (p2,T)) * ((( HT (p1,T)) / ( HT (p1,T))) *' p1)) - (( HC (p1,T)) * (b *' p2))) by Th6

      .= ( S-Poly (p1,p2,T)) by A1, A2, A8, Def1;

      hence thesis by A7, POLYRED:def 10;

    end;

    theorem :: GROEB_2:23

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

    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: G is_Groebner_basis_wrt T;

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

      

       A2: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      per cases ;

        suppose G = {} ;

        hence thesis;

      end;

        suppose G <> {} ;

        then

        reconsider G as non empty Subset of ( Polynom-Ring (n,L));

        

         A3: R is locally-confluent by A1, GROEB_1:def 3;

        now

           A4:

          now

            assume not ( 0_ (n,L)) is_a_normal_form_wrt R;

            then

            consider b be object such that

             A5: [( 0_ (n,L)), b] in R by REWRITE1:def 5;

            consider f1,f2 be object such that

             A6: f1 in ( NonZero ( Polynom-Ring (n,L))) and f2 in the carrier of ( Polynom-Ring (n,L)) and

             A7: [( 0_ (n,L)), b] = [f1, f2] by A5, ZFMISC_1:def 2;

            

             A8: f1 = ( 0_ (n,L)) by A7, XTUPLE_0: 1;

             not f1 in {( 0_ (n,L))} by A2, A6, XBOOLE_0:def 5;

            hence contradiction by A8, TARSKI:def 1;

          end;

          let g1,g2,h be Polynomial of n, L;

          assume that

           A9: g1 in G & g2 in G and

           A10: h is_a_normal_form_of (( S-Poly (g1,g2,T)),R);

          ( S-Poly (g1,g2,T)) in (G -Ideal ) by A9, Th18;

          then R reduces (( S-Poly (g1,g2,T)),( 0_ (n,L))) by A3, GROEB_1: 15;

          then

           A11: (( S-Poly (g1,g2,T)),( 0_ (n,L))) are_convertible_wrt R by REWRITE1: 25;

          R reduces (( S-Poly (g1,g2,T)),h) by A10, REWRITE1:def 6;

          then (h,( S-Poly (g1,g2,T))) are_convertible_wrt R by REWRITE1: 25;

          then

           A12: (h,( 0_ (n,L))) are_convertible_wrt R by A11, REWRITE1: 30;

          h is_a_normal_form_wrt R by A10, REWRITE1:def 6;

          hence h = ( 0_ (n,L)) by A3, A4, A12, REWRITE1:def 19;

        end;

        hence thesis;

      end;

    end;

    theorem :: GROEB_2:24

    for n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L)) holds (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))) implies (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 n be Element of NAT , T be connected admissible TermOrder of n, L be Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L));

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

      assume

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

      now

        let g1,g2 be Polynomial of n, L;

        now

          per cases ;

            case ( S-Poly (g1,g2,T)) in ( field R);

            hence ( S-Poly (g1,g2,T)) has_a_normal_form_wrt R by REWRITE1:def 14;

          end;

            case not ( S-Poly (g1,g2,T)) in ( field R);

            hence ( S-Poly (g1,g2,T)) has_a_normal_form_wrt R by REWRITE1: 46;

          end;

        end;

        then

        consider q be object such that

         A2: q is_a_normal_form_of (( S-Poly (g1,g2,T)),R) by REWRITE1:def 11;

        R reduces (( S-Poly (g1,g2,T)),q) by A2, REWRITE1:def 6;

        then

        reconsider q as Polynomial of n, L by Lm1;

        assume g1 in G & g2 in G;

        then q = ( 0_ (n,L)) by A1, A2;

        hence R reduces (( S-Poly (g1,g2,T)),( 0_ (n,L))) by A2, REWRITE1:def 6;

      end;

      hence thesis;

    end;

    theorem :: GROEB_2:25

    

     Th25: for n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, 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 holds ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L)))) implies G is_Groebner_basis_wrt T

    proof

      let n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, 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 holds ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L)));

      now

        let g1,g2 be Polynomial of n, L;

        assume that g1 <> g2 and

         A3: g1 in G and

         A4: g2 in G;

        thus for m1,m2 be Monomial of n, L st ( HM ((m1 *' g1),T)) = ( HM ((m2 *' g2),T)) holds ( PolyRedRel (G,T)) reduces (((m1 *' g1) - (m2 *' g2)),( 0_ (n,L)))

        proof

          set a1 = ( HC (g1,T)), a2 = ( HC (g2,T));

          set t1 = ( HT (g1,T)), t2 = ( HT (g2,T));

          let m1,m2 be Monomial of n, L;

          assume

           A5: ( HM ((m1 *' g1),T)) = ( HM ((m2 *' g2),T));

          

           A6: a2 <> ( 0. L) by A1, A4, TERMORD: 17;

          reconsider g1, g2 as non-zero Polynomial of n, L by A1, A3, A4, POLYNOM7:def 1;

          set b1 = ( coefficient m1), b2 = ( coefficient m2);

          set u1 = ( term m1), u2 = ( term m2);

          

           A7: a1 <> ( 0. L) by A1, A3, TERMORD: 17;

          then

          reconsider a1, a2 as non zero Element of L by A6, STRUCT_0:def 12;

          

           A8: ( HC ((m1 *' g1),T)) = ( coefficient ( HM ((m1 *' g1),T))) by TERMORD: 22

          .= ( HC ((m2 *' g2),T)) by A5, TERMORD: 22;

          now

            per cases ;

              case

               A9: b1 = ( 0. L) or b2 = ( 0. L);

              now

                per cases by A9;

                  case b1 = ( 0. L);

                  then ( HC (m1,T)) = ( 0. L) by TERMORD: 23;

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

                  then

                   A10: (m1 *' g1) = ( 0_ (n,L)) by POLYRED: 5;

                  then ( HC ((m2 *' g2),T)) = ( 0. L) by A8, TERMORD: 17;

                  then (m2 *' g2) = ( 0_ (n,L)) by TERMORD: 17;

                  then ((m1 *' g1) - (m2 *' g2)) = ( 0_ (n,L)) by A10, POLYRED: 4;

                  hence thesis by REWRITE1: 12;

                end;

                  case b2 = ( 0. L);

                  then ( HC (m2,T)) = ( 0. L) by TERMORD: 23;

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

                  then

                   A11: (m2 *' g2) = ( 0_ (n,L)) by POLYRED: 5;

                  then ( HC ((m1 *' g1),T)) = ( 0. L) by A8, TERMORD: 17;

                  then (m1 *' g1) = ( 0_ (n,L)) by TERMORD: 17;

                  then ((m1 *' g1) - (m2 *' g2)) = ( 0_ (n,L)) by A11, POLYRED: 4;

                  hence thesis by REWRITE1: 12;

                end;

              end;

              hence thesis;

            end;

              case

               A12: b1 <> ( 0. L) & b2 <> ( 0. L);

              then

              reconsider b1, b2 as non zero Element of L by STRUCT_0:def 12;

              (b2 * a2) <> ( 0. L) by VECTSP_2:def 1;

              then

               A13: (b2 * a2) is non zero;

              t1 divides ( lcm (t1,t2)) by Th3;

              then

              consider s1 be bag of n such that

               A14: (t1 + s1) = ( lcm (t1,t2)) by TERMORD: 1;

              ( HC (m2,T)) <> ( 0. L) by A12, TERMORD: 23;

              then

               A15: m2 <> ( 0_ (n,L)) by TERMORD: 17;

              ( HC (m1,T)) <> ( 0. L) by A12, TERMORD: 23;

              then m1 <> ( 0_ (n,L)) by TERMORD: 17;

              then

              reconsider m1, m2 as non-zero Monomial of n, L by A15, POLYNOM7:def 1;

              

               A16: ( Monom ((b1 * a1),(u1 + t1))) = (( Monom (b1,u1)) *' ( Monom (a1,t1))) by TERMORD: 3

              .= (m1 *' ( Monom (a1,t1))) by POLYNOM7: 11

              .= (( HM (m1,T)) *' ( Monom (a1,t1))) by TERMORD: 23

              .= (( HM (m1,T)) *' ( HM (g1,T))) by TERMORD:def 8

              .= ( HM ((m2 *' g2),T)) by A5, TERMORD: 33

              .= (( HM (m2,T)) *' ( HM (g2,T))) by TERMORD: 33

              .= (( HM (m2,T)) *' ( Monom (a2,t2))) by TERMORD:def 8

              .= (m2 *' ( Monom (a2,t2))) by TERMORD: 23

              .= (( Monom (b2,u2)) *' ( Monom (a2,t2))) by POLYNOM7: 11

              .= ( Monom ((b2 * a2),(u2 + t2))) by TERMORD: 3;

              

              then (b1 * a1) = ( coefficient ( Monom ((b2 * a2),(u2 + t2)))) by POLYNOM7: 9

              .= (b2 * a2) by POLYNOM7: 9;

              

              then ((b1 * a1) / a2) = ((b2 * a2) * (a2 " ))

              .= (b2 * (a2 * (a2 " ))) by GROUP_1:def 3

              .= (b2 * ( 1. L)) by A6, VECTSP_1:def 10;

              

              then

               A17: (b2 / a1) = (((b1 * a1) / a2) / a1)

              .= (((b1 * a1) * (a2 " )) / a1)

              .= (((b1 * a1) * (a2 " )) * (a1 " ))

              .= (((b1 * (a2 " )) * a1) * (a1 " )) by GROUP_1:def 3

              .= ((b1 * (a2 " )) * (a1 * (a1 " ))) by GROUP_1:def 3

              .= ((b1 * (a2 " )) * ( 1. L)) by A7, VECTSP_1:def 10

              .= (b1 * (a2 " ))

              .= (b1 / a2);

              (b1 * a1) <> ( 0. L) by VECTSP_2:def 1;

              then (b1 * a1) is non zero;

              

              then

               A18: (u1 + t1) = ( term ( Monom ((b2 * a2),(u2 + t2)))) by A16, POLYNOM7: 10

              .= (u2 + t2) by A13, POLYNOM7: 10;

              then t1 divides (u1 + t1) & t2 divides (u1 + t1) by TERMORD: 1;

              then ( lcm (t1,t2)) divides (u1 + t1) by Th4;

              then

              consider v be bag of n such that

               A19: (u1 + t1) = (( lcm (t1,t2)) + v) by TERMORD: 1;

              (u1 + t1) = ((v + s1) + t1) by A14, A19, PRE_POLY: 35;

              

              then

               A20: u1 = (((v + s1) + t1) -' t1) by PRE_POLY: 48

              .= (v + s1) by PRE_POLY: 48;

              t2 divides ( lcm (t1,t2)) by Th3;

              then

              consider s2 be bag of n such that

               A21: (t2 + s2) = ( lcm (t1,t2)) by TERMORD: 1;

              (u2 + t2) = ((v + s2) + t2) by A18, A21, A19, PRE_POLY: 35;

              

              then

               A22: u2 = (((v + s2) + t2) -' t2) by PRE_POLY: 48

              .= (v + s2) by PRE_POLY: 48;

              ( HT (g2,T)) divides ( lcm (( HT (g1,T)),( HT (g2,T)))) by Th3;

              then

               A23: s2 = (( lcm (( HT (g1,T)),( HT (g2,T)))) / ( HT (g2,T))) by A21, Def1;

              

               A24: ((b2 / a1) * a1) = ((b2 * (a1 " )) * a1)

              .= (b2 * ((a1 " ) * a1)) by GROUP_1:def 3

              .= (b2 * ( 1. L)) by A7, VECTSP_1:def 10

              .= b2;

              ( HT (g1,T)) divides ( lcm (( HT (g1,T)),( HT (g2,T)))) by Th3;

              then

               A25: s1 = (( lcm (( HT (g1,T)),( HT (g2,T)))) / ( HT (g1,T))) by A14, Def1;

              

               A26: ((b1 / a2) * a2) = ((b1 * (a2 " )) * a2)

              .= (b1 * ((a2 " ) * a2)) by GROUP_1:def 3

              .= (b1 * ( 1. L)) by A6, VECTSP_1:def 10;

              ((m1 *' g1) - (m2 *' g2)) = ((( Monom (b1,u1)) *' g1) - (m2 *' g2)) by POLYNOM7: 11

              .= ((( Monom (b1,u1)) *' g1) - (( Monom (b2,u2)) *' g2)) by POLYNOM7: 11

              .= ((b1 * ((v + s1) *' g1)) - (( Monom (b2,(v + s2))) *' g2)) by A20, A22, POLYRED: 22

              .= ((b1 * (v *' (s1 *' g1))) - (( Monom (b2,(v + s2))) *' g2)) by POLYRED: 18

              .= ((b1 * (v *' (s1 *' g1))) - (b2 * ((v + s2) *' g2))) by POLYRED: 22

              .= ((b1 * (v *' (s1 *' g1))) - (b2 * (v *' (s2 *' g2)))) by POLYRED: 18

              .= ((b1 * (v *' (s1 *' g1))) + ( - (b2 * (v *' (s2 *' g2))))) by POLYNOM1:def 7

              .= ((b1 * (v *' (s1 *' g1))) + (b2 * ( - (v *' (s2 *' g2))))) by POLYRED: 9

              .= ((((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * ( - (v *' (s2 *' g2))))) by A26, A24

              .= ((((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (v *' ( - (s2 *' g2))))) by Th13

              .= ((((b1 / a2) * a2) * (v *' (s1 *' g1))) + ((b1 / a2) * (a1 * (v *' ( - (s2 *' g2)))))) by A17, POLYRED: 11

              .= (((b1 / a2) * (a2 * (v *' (s1 *' g1)))) + ((b1 / a2) * (a1 * (v *' ( - (s2 *' g2)))))) by POLYRED: 11

              .= ((b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (a1 * (v *' ( - (s2 *' g2)))))) by Th15

              .= ((b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (a1 * ( - (s2 *' g2)))))) by Th14

              .= ((b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' ( - (a1 * (s2 *' g2)))))) by POLYRED: 9

              .= ((b1 / a2) * ((v *' (a2 * (s1 *' g1))) + (v *' ( - (a1 * (s2 *' g2)))))) by Th14

              .= ((b1 / a2) * (v *' ((a2 * (s1 *' g1)) + ( - (a1 * (s2 *' g2)))))) by Th12

              .= ((b1 / a2) * (v *' ( S-Poly (g1,g2,T)))) by A25, A23, POLYNOM1:def 7

              .= (( Monom ((b1 / a2),v)) *' ( S-Poly (g1,g2,T))) by POLYRED: 22;

              hence thesis by A2, A3, A4, POLYRED: 48;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis by Th17;

    end;

    definition

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

      :: GROEB_2:def5

      func S-Poly (P,T) -> Subset of ( Polynom-Ring (n,L)) equals { ( S-Poly (p1,p2,T)) where p1,p2 be Polynomial of n, L : p1 in P & p2 in P };

      coherence

      proof

        set M = { ( S-Poly (p1,p2,T)) where p1,p2 be Polynomial of n, L : p1 in P & p2 in P };

        now

          let u be object;

          assume u in M;

          then ex p1,p2 be Polynomial of n, L st u = ( S-Poly (p1,p2,T)) & p1 in P & p2 in P;

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

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      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 finite Subset of ( Polynom-Ring (n,L));

      cluster ( S-Poly (P,T)) -> finite;

      coherence

      proof

        defpred P[ object, object] means ex p1,p2 be Polynomial of n, L st p1 = ($1 `1 ) & ($1 `2 ) = p2 & p1 in P & p2 in P & $2 = ( S-Poly (p1,p2,T));

        

         A1: for x be object st x in [:P, P:] holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in [:P, P:];

          then

          consider p1,p2 be object such that

           A2: p1 in P & p2 in P and

           A3: [p1, p2] = x by ZFMISC_1:def 2;

          reconsider p1, p2 as Polynomial of n, L by A2, POLYNOM1:def 11;

          take ( S-Poly (p1,p2,T));

          take p1, p2;

          thus (x `1 ) = p1 by A3;

          thus (x `2 ) = p2 by A3;

          thus thesis by A2;

        end;

        consider f be Function such that

         A4: ( dom f) = [:P, P:] & for x be object st x in [:P, P:] holds P[x, (f . x)] from CLASSES1:sch 1( A1);

         A5:

        now

          let v be object;

          assume v in ( S-Poly (P,T));

          then

          consider p1,p2 be Polynomial of n, L such that

           A6: v = ( S-Poly (p1,p2,T)) and

           A7: p1 in P & p2 in P;

          

           A8: [p1, p2] in ( dom f) by A4, A7, ZFMISC_1:def 2;

          then

          consider p19,p29 be Polynomial of n, L such that

           A9: ( [p1, p2] `1 ) = p19 & ( [p1, p2] `2 ) = p29 and p19 in P and p29 in P and

           A10: (f . [p1, p2]) = ( S-Poly (p19,p29,T)) by A4;

          p1 = p19 & p2 = p29 by A9;

          hence v in ( rng f) by A6, A8, A10, FUNCT_1:def 3;

        end;

        now

          let v be object;

          assume v in ( rng f);

          then

          consider u be object such that

           A11: u in ( dom f) and

           A12: v = (f . u) by FUNCT_1:def 3;

          ex p1,p2 be Polynomial of n, L st p1 = (u `1 ) & (u `2 ) = p2 & p1 in P & p2 in P & (f . u) = ( S-Poly (p1,p2,T)) by A4, A11;

          hence v in ( S-Poly (P,T)) by A12;

        end;

        then ( rng f) = ( S-Poly (P,T)) by A5, TARSKI: 2;

        hence thesis by A4, FINSET_1: 8;

      end;

    end

    theorem :: GROEB_2:26

    for n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L)) st not (( 0_ (n,L)) in G) & for g be Polynomial of n, L st g in G holds g is Monomial of n, L holds G is_Groebner_basis_wrt T

    proof

      let n be Element of NAT , T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, G be Subset of ( Polynom-Ring (n,L));

      assume that

       A1: not ( 0_ (n,L)) in G and

       A2: for g be Polynomial of n, L st g in G holds g is Monomial of n, L;

      now

        let g1,g2 be Polynomial of n, L;

        assume g1 in G & g2 in G;

        then g1 is Monomial of n, L & g2 is Monomial of n, L by A2;

        then ( S-Poly (g1,g2,T)) = ( 0_ (n,L)) by Th19;

        hence ( PolyRedRel (G,T)) reduces (( S-Poly (g1,g2,T)),( 0_ (n,L))) by REWRITE1: 12;

      end;

      hence thesis by A1, Th25;

    end;

    begin

    theorem :: GROEB_2:27

    for L be non empty multLoopStr, P be non empty Subset of L, A be LeftLinearCombination of P, i be Element of NAT holds (A | i) is LeftLinearCombination of P

    proof

      let L be non empty multLoopStr, P be non empty Subset of L, A be LeftLinearCombination of P, j be Element of NAT ;

      set C = (A | ( Seg j));

      reconsider C as FinSequence of the carrier of L by FINSEQ_1: 18;

      now

        let i be set;

        

         A1: ( dom C) c= ( dom A) by RELAT_1: 60;

        assume

         A2: i in ( dom C);

        then (C . i) = (A . i) by FUNCT_1: 47;

        

        then (C /. i) = (A . i) by A2, PARTFUN1:def 6

        .= (A /. i) by A2, A1, PARTFUN1:def 6;

        hence ex u be Element of L, a be Element of P st (C /. i) = (u * a) by A2, A1, IDEAL_1:def 9;

      end;

      then C is LeftLinearCombination of P by IDEAL_1:def 9;

      hence thesis by FINSEQ_1:def 15;

    end;

    theorem :: GROEB_2:28

    for L be non empty multLoopStr, P be non empty Subset of L, A be LeftLinearCombination of P, i be Element of NAT holds (A /^ i) is LeftLinearCombination of P

    proof

      let L be non empty multLoopStr, P be non empty Subset of L, A be LeftLinearCombination of P, j be Element of NAT ;

      set C = (A /^ j);

      reconsider C as FinSequence of the carrier of L;

      now

        per cases ;

          case

           A1: j <= ( len A);

          then

          reconsider m = (( len A) - j) as Element of NAT by INT_1: 5;

          now

            let i be set;

            assume

             A2: i in ( dom C);

            then

            reconsider k = i as Element of NAT ;

            

             A3: ( dom C) = ( Seg ( len C)) by FINSEQ_1:def 3

            .= ( Seg m) by A1, RFINSEQ:def 1;

            then k <= (( len A) - j) by A2, FINSEQ_1: 1;

            then

             A4: (k + j) <= ((( len A) + ( - j)) + j) by XREAL_1: 6;

            

             A5: k <= (k + j) by NAT_1: 11;

            1 <= k by A2, A3, FINSEQ_1: 1;

            then 1 <= (k + j) by A5, XXREAL_0: 2;

            then (j + k) in ( Seg ( len A)) by A4, FINSEQ_1: 1;

            then (j + k) in ( dom A) by FINSEQ_1:def 3;

            then ex u be Element of L, a be Element of P st (A /. (j + k)) = (u * a) by IDEAL_1:def 9;

            hence ex u be Element of L, a be Element of P st (C /. i) = (u * a) by A2, FINSEQ_5: 27;

          end;

          hence thesis by IDEAL_1:def 9;

        end;

          case not j <= ( len A);

          then C = ( <*> the carrier of L) by RFINSEQ:def 1;

          then for i be set st i in ( dom C) holds ex u be Element of L, a be Element of P st (C /. i) = (u * a);

          hence thesis by IDEAL_1:def 9;

        end;

      end;

      hence thesis;

    end;

    theorem :: GROEB_2:29

    for L be non empty multLoopStr, P,Q be non empty Subset of L, A be LeftLinearCombination of P holds P c= Q implies A is LeftLinearCombination of Q

    proof

      let L be non empty multLoopStr, P,Q be non empty Subset of L, A be LeftLinearCombination of P;

      assume

       A1: P c= Q;

      now

        let i be set;

        assume i in ( dom A);

        then

        consider u be Element of L, a be Element of P such that

         A2: (A /. i) = (u * a) by IDEAL_1:def 9;

        a in P;

        hence ex u be Element of L, a be Element of Q st (A /. i) = (u * a) by A1, A2;

      end;

      hence thesis by IDEAL_1:def 9;

    end;

    definition

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P;

      :: original: ^

      redefine

      func A ^ B -> LeftLinearCombination of P ;

      coherence

      proof

        (A ^ B) is LeftLinearCombination of (P \/ P);

        hence thesis;

      end;

    end

    definition

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P;

      :: GROEB_2:def6

      pred A is_MonomialRepresentation_of f means ( Sum A) = f & for i be Element of NAT st i in ( dom A) holds ex m be Monomial of n, L, p be Polynomial of n, L st p in P & (A /. i) = (m *' p);

    end

    theorem :: GROEB_2:30

    for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P st A is_MonomialRepresentation_of f holds ( Support f) c= ( union { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) })

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P;

      assume

       A1: A is_MonomialRepresentation_of f;

      defpred P[ Nat] means for f be Polynomial of n, L, A be LeftLinearCombination of P st A is_MonomialRepresentation_of f & ( len A) = $1 holds ( Support f) c= ( union { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) });

      

       A2: ex n be Element of NAT st ( len A) = n;

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        for f be Polynomial of n, L, A be LeftLinearCombination of P st A is_MonomialRepresentation_of f & ( len A) = (k + 1) holds ( Support f) c= ( union { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) })

        proof

          

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

          let f be Polynomial of n, L, A be LeftLinearCombination of P;

          assume that

           A6: A is_MonomialRepresentation_of f and

           A7: ( len A) = (k + 1);

          

           A8: A <> ( <*> the carrier of ( Polynom-Ring (n,L))) by A7;

          

           A9: ( Sum A) = f by A6;

          reconsider A as non empty LeftLinearCombination of P by A8;

          consider A9 be LeftLinearCombination of P, e be Element of ( Polynom-Ring (n,L)) such that

           A10: A = (A9 ^ <*e*>) and <*e*> is LeftLinearCombination of P by IDEAL_1: 33;

          

           A11: ( dom A) = ( Seg (k + 1)) by A7, FINSEQ_1:def 3;

          reconsider ep = ( Sum <*e*>) as Polynomial of n, L by POLYNOM1:def 11;

          reconsider g = ( Sum A9) as Polynomial of n, L by POLYNOM1:def 11;

          f = (( Sum A9) + ( Sum <*e*>)) by A9, A10, RLVECT_1: 41

          .= (g + ep) by POLYNOM1:def 11;

          then

           A12: ( Support f) c= (( Support g) \/ ( Support ep)) by POLYNOM1: 20;

          

           A13: ( len A) = (( len A9) + ( len <*e*>)) by A10, FINSEQ_1: 22

          .= (( len A9) + 1) by FINSEQ_1: 39;

          then ( dom A9) = ( Seg k) by A7, FINSEQ_1:def 3;

          then

           A14: ( dom A9) c= ( dom A) by A11, A5, FINSEQ_1: 5;

          now

            let i be Element of NAT ;

            assume

             A15: i in ( dom A9);

            

            then (A /. i) = (A . i) by A14, PARTFUN1:def 6

            .= (A9 . i) by A10, A15, FINSEQ_1:def 7

            .= (A9 /. i) by A15, PARTFUN1:def 6;

            hence ex m be Monomial of n, L, p be Polynomial of n, L st p in P & (A9 /. i) = (m *' p) by A6, A14, A15;

          end;

          then A9 is_MonomialRepresentation_of g;

          then

           A16: ( Support g) c= ( union { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A9) & (A9 /. i) = (m *' p) }) by A4, A7, A13;

          now

            let x be object;

            assume

             A17: x in ( Support f);

            then

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

            now

              per cases by A12, A17, XBOOLE_0:def 3;

                case u in ( Support g);

                then

                consider Y be set such that

                 A18: u in Y and

                 A19: Y in { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A9) & (A9 /. i) = (m *' p) } by A16, TARSKI:def 4;

                consider m9 be Monomial of n, L, p9 be Polynomial of n, L such that

                 A20: Y = ( Support (m9 *' p9)) and

                 A21: ex i be Element of NAT st i in ( dom A9) & (A9 /. i) = (m9 *' p9) by A19;

                consider i be Element of NAT such that

                 A22: i in ( dom A9) and

                 A23: (A9 /. i) = (m9 *' p9) by A21;

                (A /. i) = (A . i) by A14, A22, PARTFUN1:def 6

                .= (A9 . i) by A10, A22, FINSEQ_1:def 7

                .= (A9 /. i) by A22, PARTFUN1:def 6;

                then Y in { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) } by A14, A20, A22, A23;

                hence u in ( union { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) }) by A18, TARSKI:def 4;

              end;

                case

                 A24: u in ( Support ep);

                1 <= ( len A) by A7, NAT_1: 11;

                then

                 A25: ( len A) in ( Seg ( len A)) by FINSEQ_1: 1;

                ( dom A) = ( Seg ( len A)) by FINSEQ_1:def 3;

                then

                 A26: ex m9 be Monomial of n, L, p9 be Polynomial of n, L st p9 in P & (A /. ( len A)) = (m9 *' p9) by A6, A25;

                

                 A27: (A . ( len A)) = e & e = ( Sum <*e*>) by A10, A13, FINSEQ_1: 42, RLVECT_1: 44;

                

                 A28: ( len A) in ( dom A) by A25, FINSEQ_1:def 3;

                then (A /. ( len A)) = (A . ( len A)) by PARTFUN1:def 6;

                then ( Support ep) in { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) } by A28, A26, A27;

                hence u in ( union { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) }) by A24, TARSKI:def 4;

              end;

            end;

            hence x in ( union { ( Support (m *' p)) where m be Monomial of n, L, p be Polynomial of n, L : ex i be Element of NAT st i in ( dom A) & (A /. i) = (m *' p) });

          end;

          hence thesis by TARSKI:def 3;

        end;

        hence P[(k + 1)];

      end;

      

       A29: P[ 0 ]

      proof

        let f be Polynomial of n, L, A be LeftLinearCombination of P;

        assume that

         A30: A is_MonomialRepresentation_of f and

         A31: ( len A) = 0 ;

        A = ( <*> the carrier of ( Polynom-Ring (n,L))) by A31;

        then ( Sum A) = ( 0. ( Polynom-Ring (n,L))) by RLVECT_1: 43;

        then f = ( 0. ( Polynom-Ring (n,L))) by A30;

        then f = ( 0_ (n,L)) by POLYNOM1:def 11;

        then ( Support f) = {} by POLYNOM7: 1;

        hence thesis by XBOOLE_1: 2;

      end;

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

      hence thesis by A1, A2;

    end;

    theorem :: GROEB_2:31

    for n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P st A is_MonomialRepresentation_of f & B is_MonomialRepresentation_of g holds (A ^ B) is_MonomialRepresentation_of (f + g)

    proof

      let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P;

      assume that

       A1: A is_MonomialRepresentation_of f and

       A2: B is_MonomialRepresentation_of g;

       A3:

      now

        let i be Element of NAT ;

        assume

         A4: i in ( dom (A ^ B));

        now

          per cases by A4, FINSEQ_1: 25;

            case

             A5: i in ( dom A);

            ( dom A) c= ( dom (A ^ B)) by FINSEQ_1: 26;

            

            then ((A ^ B) /. i) = ((A ^ B) . i) by A5, PARTFUN1:def 6

            .= (A . i) by A5, FINSEQ_1:def 7

            .= (A /. i) by A5, PARTFUN1:def 6;

            hence ex m be Monomial of n, L, p be Polynomial of n, L st p in P & ((A ^ B) /. i) = (m *' p) by A1, A5;

          end;

            case ex k be Nat st k in ( dom B) & i = (( len A) + k);

            then

            consider k be Nat such that

             A6: k in ( dom B) and

             A7: i = (( len A) + k);

            i in ( dom (A ^ B)) by A6, A7, FINSEQ_1: 28;

            

            then ((A ^ B) /. i) = ((A ^ B) . i) by PARTFUN1:def 6

            .= (B . k) by A6, A7, FINSEQ_1:def 7

            .= (B /. k) by A6, PARTFUN1:def 6;

            hence ex m be Monomial of n, L, p be Polynomial of n, L st p in P & ((A ^ B) /. i) = (m *' p) by A2, A6;

          end;

        end;

        hence ex m be Monomial of n, L, p be Polynomial of n, L st p in P & ((A ^ B) /. i) = (m *' p);

      end;

      reconsider f9 = f, g9 = g as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      reconsider f9, g9 as Element of ( Polynom-Ring (n,L));

      ( Sum (A ^ B)) = (( Sum A) + ( Sum B)) by RLVECT_1: 41

      .= (f9 + ( Sum B)) by A1

      .= (f9 + g9) by A2

      .= (f + g) by POLYNOM1:def 11;

      hence thesis by A3;

    end;

    

     Lm4: for n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P st A is_MonomialRepresentation_of f holds for b be bag of n holds (for i be Element of NAT st i in ( dom A) holds for m be Monomial of n, L, p be Polynomial of n, L st (A . i) = (m *' p) & p in P holds ((m *' p) . b) = ( 0. L)) implies (f . b) = ( 0. L)

    proof

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

      assume

       A1: A is_MonomialRepresentation_of f;

      let b be bag of n;

      assume

       A2: for i be Element of NAT st i in ( dom A) holds for m be Monomial of n, L, p be Polynomial of n, L st (A . i) = (m *' p) & p in P holds ((m *' p) . b) = ( 0. L);

      defpred P[ Nat] means for f be Polynomial of n, L, A be LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = ( Sum A) & ( len A) = $1 holds (for i be Element of NAT st i in ( dom A) holds for m be Monomial of n, L, p be Polynomial of n, L st (A . i) = (m *' p) & p in P holds ((m *' p) . b) = ( 0. L)) implies (f . b) = ( 0. L);

       A3:

      now

        let k be Nat;

        assume

         A4: P[k];

        for f be Polynomial of n, L, A be LeftLinearCombination of P st A is_MonomialRepresentation_of f & f = ( Sum A) & ( len A) = (k + 1) holds (for i be Element of NAT st i in ( dom A) holds for m be Monomial of n, L, p be Polynomial of n, L st (A . i) = (m *' p) & p in P holds ((m *' p) . b) = ( 0. L)) implies (f . b) = ( 0. L)

        proof

          let f be Polynomial of n, L, A be LeftLinearCombination of P;

          assume that

           A5: A is_MonomialRepresentation_of f and

           A6: f = ( Sum A) and

           A7: ( len A) = (k + 1);

          set B = (A | ( Seg k));

          reconsider B as FinSequence of ( Polynom-Ring (n,L)) by FINSEQ_1: 18;

          reconsider B as LeftLinearCombination of P by IDEAL_1: 42;

          set g = ( Sum B);

          reconsider g as Polynomial of n, L by POLYNOM1:def 11;

          

           A8: ( dom A) = ( Seg (k + 1)) by A7, FINSEQ_1:def 3;

          then (k + 1) in ( dom A) by FINSEQ_1: 4;

          then

           A9: ex m be Monomial of n, L, p be Polynomial of n, L st p in P & (A /. (k + 1)) = (m *' p) by A5;

          

           A10: k <= ( len A) by A7, NAT_1: 11;

          then k <= (k + 1) & ( dom B) = ( Seg k) by FINSEQ_1: 17, NAT_1: 11;

          then

           A11: ( dom B) c= ( dom A) by A8, FINSEQ_1: 5;

          now

            let i be Element of NAT ;

            assume

             A12: i in ( dom B);

            

            then (B /. i) = (B . i) by PARTFUN1:def 6

            .= (A . i) by A12, FUNCT_1: 47

            .= (A /. i) by A11, A12, PARTFUN1:def 6;

            hence ex m be Monomial of n, L, p be Polynomial of n, L st p in P & (B /. i) = (m *' p) by A5, A11, A12;

          end;

          then

           A13: B is_MonomialRepresentation_of g;

          assume

           A14: for i be Element of NAT st i in ( dom A) holds for m be Monomial of n, L, p be Polynomial of n, L st (A . i) = (m *' p) & p in P holds ((m *' p) . b) = ( 0. L);

           A15:

          now

            let i be Element of NAT ;

            assume

             A16: i in ( dom B);

            now

              let m be Monomial of n, L, p be Polynomial of n, L;

              assume that

               A17: (B . i) = (m *' p) and

               A18: p in P;

              (A . i) = (m *' p) by A16, A17, FUNCT_1: 47;

              hence ((m *' p) . b) = ( 0. L) by A14, A11, A16, A18;

            end;

            hence for m be Monomial of n, L, p be Polynomial of n, L st (B . i) = (m *' p) & p in P holds ((m *' p) . b) = ( 0. L);

          end;

          reconsider h = (A /. (k + 1)) as Polynomial of n, L by POLYNOM1:def 11;

          (B ^ <*(A /. (k + 1))*>) = (B ^ <*(A . (k + 1))*>) by A8, FINSEQ_1: 4, PARTFUN1:def 6

          .= A by A7, FINSEQ_3: 55;

          

          then f = (( Sum B) + ( Sum <*(A /. (k + 1))*>)) by A6, RLVECT_1: 41

          .= (( Sum B) + (A /. (k + 1))) by RLVECT_1: 44

          .= (g + h) by POLYNOM1:def 11;

          then

           A19: (f . b) = ((g . b) + (h . b)) by POLYNOM1: 15;

          (A /. (k + 1)) = (A . (k + 1)) by A8, FINSEQ_1: 4, PARTFUN1:def 6;

          then

           A20: ( 0. L) = (h . b) by A14, A8, A9, FINSEQ_1: 4;

          ( len B) = k by A10, FINSEQ_1: 17;

          then (g . b) = ( 0. L) by A4, A13, A15;

          hence thesis by A19, A20, RLVECT_1:def 4;

        end;

        hence P[(k + 1)];

      end;

      

       A21: P[ 0 ]

      proof

        let f be Polynomial of n, L, A be LeftLinearCombination of P;

        assume that A is_MonomialRepresentation_of f and

         A22: f = ( Sum A) & ( len A) = 0 ;

        assume for i be Element of NAT st i in ( dom A) holds for m be Monomial of n, L, p be Polynomial of n, L st (A . i) = (m *' p) & p in P holds ((m *' p) . b) = ( 0. L);

        A = ( <*> the carrier of ( Polynom-Ring (n,L))) by A22;

        

        then f = ( Sum ( <*> the carrier of ( Polynom-Ring (n,L)))) by A22

        .= ( 0. ( Polynom-Ring (n,L))) by RLVECT_1: 43

        .= ( 0_ (n,L)) by POLYNOM1:def 11;

        hence thesis by POLYNOM1: 22;

      end;

      

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

      

       A24: ex n be Element of NAT st n = ( len A);

      thus thesis by A1, A2, A23, A24;

    end;

    definition

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P, b be bag of n;

      :: GROEB_2:def7

      pred A is_Standard_Representation_of f,P,b,T means ( Sum A) = f & for i be Element of NAT st i in ( dom A) holds ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A /. i) = (m *' p) & ( HT ((m *' p),T)) <= (b,T);

    end

    definition

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

      :: GROEB_2:def8

      pred A is_Standard_Representation_of f,P,T means A is_Standard_Representation_of (f,P,( HT (f,T)),T);

    end

    definition

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

      :: GROEB_2:def9

      pred f has_a_Standard_Representation_of P,b,T means ex A be LeftLinearCombination of P st A is_Standard_Representation_of (f,P,b,T);

    end

    definition

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

      :: GROEB_2:def10

      pred f has_a_Standard_Representation_of P,T means ex A be LeftLinearCombination of P st A is_Standard_Representation_of (f,P,T);

    end

    theorem :: GROEB_2:32

    

     Th32: for n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P, b be bag of n holds A is_Standard_Representation_of (f,P,b,T) implies A is_MonomialRepresentation_of f

    proof

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P, b be bag of n;

      assume

       A1: A is_Standard_Representation_of (f,P,b,T);

       A2:

      now

        let i be Element of NAT ;

        assume i in ( dom A);

        then ex m9 be non-zero Monomial of n, L, p9 be non-zero Polynomial of n, L st p9 in P & (A /. i) = (m9 *' p9) & ( HT ((m9 *' p9),T)) <= (b,T) by A1;

        hence ex m be Monomial of n, L, p be Polynomial of n, L st p in P & (A /. i) = (m *' p);

      end;

      ( Sum A) = f by A1;

      hence thesis by A2;

    end;

    

     Lm5: for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L)) st f = f9 & g = g9 holds for P be non empty Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) reduces (f,g) implies ex A be LeftLinearCombination of P st f9 = (g9 + ( Sum A)) & for i be Element of NAT st i in ( dom A) holds ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T)

    proof

      let n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f,g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L));

      assume

       A1: f = f9 & g = g9;

      defpred P[ Nat] means for f,g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L)) st f = f9 & g = g9 holds for P be non empty Subset of ( Polynom-Ring (n,L)), R be RedSequence of ( PolyRedRel (P,T)) st (R . 1) = f & (R . ( len R)) = g & ( len R) = $1 holds ex A be LeftLinearCombination of P st f9 = (g9 + ( Sum A)) & for i be Element of NAT st i in ( dom A) holds ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T);

      let P be non empty Subset of ( Polynom-Ring (n,L));

      assume ( PolyRedRel (P,T)) reduces (f,g);

      then

      consider R be RedSequence of ( PolyRedRel (P,T)) such that

       A2: (R . 1) = f & (R . ( len R)) = g by REWRITE1:def 3;

      

       A3: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

       A4:

      now

        let k be Nat;

        assume

         A5: 1 <= k;

        thus P[k] implies P[(k + 1)]

        proof

          assume

           A6: P[k];

          for f,g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L)) st f = f9 & g = g9 holds for P be non empty Subset of ( Polynom-Ring (n,L)), R be RedSequence of ( PolyRedRel (P,T)) st (R . 1) = f & (R . ( len R)) = g & ( len R) = (k + 1) holds ex A be LeftLinearCombination of P st f9 = (g9 + ( Sum A)) & for i be Element of NAT st i in ( dom A) holds ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T)

          proof

            let f,g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L));

            assume that

             A7: f = f9 and

             A8: g = g9;

            let P be non empty Subset of ( Polynom-Ring (n,L)), R be RedSequence of ( PolyRedRel (P,T));

            assume that

             A9: (R . 1) = f and

             A10: (R . ( len R)) = g and

             A11: ( len R) = (k + 1);

            set Q = (R | ( Seg k));

            reconsider Q as FinSequence by FINSEQ_1: 15;

            

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

            then

             A13: ( dom Q) = ( Seg k) by A11, FINSEQ_1: 17;

            

             A14: ( dom R) = ( Seg (k + 1)) by A11, FINSEQ_1:def 3;

             A15:

            now

              let i be Nat;

              assume that

               A16: i in ( dom Q) and

               A17: (i + 1) in ( dom Q);

              (i + 1) <= k by A13, A17, FINSEQ_1: 1;

              then

               A18: (i + 1) <= (k + 1) by A12, XXREAL_0: 2;

              i <= k by A13, A16, FINSEQ_1: 1;

              then

               A19: i <= (k + 1) by A12, XXREAL_0: 2;

              1 <= (i + 1) by A13, A17, FINSEQ_1: 1;

              then

               A20: (i + 1) in ( dom R) by A14, A18, FINSEQ_1: 1;

              1 <= i by A13, A16, FINSEQ_1: 1;

              then i in ( dom R) by A14, A19, FINSEQ_1: 1;

              then

               A21: [(R . i), (R . (i + 1))] in ( PolyRedRel (P,T)) by A20, REWRITE1:def 2;

              (R . i) = (Q . i) by A16, FUNCT_1: 47;

              hence [(Q . i), (Q . (i + 1))] in ( PolyRedRel (P,T)) by A17, A21, FUNCT_1: 47;

            end;

            ( len Q) = k by A11, A12, FINSEQ_1: 17;

            then

            reconsider Q as RedSequence of ( PolyRedRel (P,T)) by A5, A15, REWRITE1:def 2;

            

             A22: 1 in ( dom Q) by A5, A13, FINSEQ_1: 1;

            then

             A23: (Q . 1) = f by A9, FUNCT_1: 47;

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

            then

             A24: (k + 1) in ( dom R) by A14, FINSEQ_1: 1;

            k in ( dom R) by A5, A14, A12, FINSEQ_1: 1;

            then

             A25: [(R . k), (R . (k + 1))] in ( PolyRedRel (P,T)) by A24, REWRITE1:def 2;

            then

            consider h9,g2 be object such that

             A26: [(R . k), (R . (k + 1))] = [h9, g2] and

             A27: h9 in ( NonZero ( Polynom-Ring (n,L))) and

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

            

             A29: (R . k) = h9 by A26, XTUPLE_0: 1;

            reconsider g2 as Polynomial of n, L by A28, POLYNOM1:def 11;

             not h9 in {( 0_ (n,L))} by A3, A27, XBOOLE_0:def 5;

            then h9 <> ( 0_ (n,L)) by TARSKI:def 1;

            then

            reconsider h9 as non-zero Polynomial of n, L by A27, POLYNOM1:def 11, POLYNOM7:def 1;

            

             A30: (Q . k) = h9 by A5, A13, A29, FINSEQ_1: 3, FUNCT_1: 47;

            then

            reconsider u9 = (Q . k) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

            reconsider u = u9 as Polynomial of n, L by POLYNOM1:def 11;

            (Q . ( len Q)) = u by A11, A12, FINSEQ_1: 17;

            then

            consider A9 be LeftLinearCombination of P such that

             A31: f9 = (u9 + ( Sum A9)) and

             A32: for i be Element of NAT st i in ( dom A9) holds ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A9 . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A6, A7, A11, A12, A23, FINSEQ_1: 17;

            

             A33: k in ( dom Q) by A5, A13, FINSEQ_1: 3;

            now

              per cases ;

                case u9 = g9;

                hence thesis by A31, A32;

              end;

                case

                 A34: u9 <> g9;

                reconsider hh = h9 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

                

                 A35: ( PolyRedRel (P,T)) reduces (f,h9) by A5, A33, A30, A22, A23, REWRITE1: 17;

                

                 A36: (R . (k + 1)) = g2 by A26, XTUPLE_0: 1;

                then

                reconsider gg = g2 as Element of ( Polynom-Ring (n,L)) by A8, A10, A11;

                h9 reduces_to (g2,P,T) by A25, A26, POLYRED:def 13;

                then

                consider p9 be Polynomial of n, L such that

                 A37: p9 in P and

                 A38: h9 reduces_to (g2,p9,T) by POLYRED:def 7;

                consider m9 be Monomial of n, L such that

                 A39: g2 = (h9 - (m9 *' p9)) and not ( HT ((m9 *' p9),T)) in ( Support g2) and

                 A40: ( HT ((m9 *' p9),T)) <= (( HT (h9,T)),T) by A38, GROEB_1: 2;

                 A41:

                now

                  assume p9 = ( 0_ (n,L));

                  

                  then g2 = (h9 - ( 0_ (n,L))) by A39, POLYRED: 5

                  .= (Q . k) by A30, POLYRED: 4;

                  hence contradiction by A8, A10, A11, A34, A36;

                end;

                 A42:

                now

                  assume m9 = ( 0_ (n,L));

                  

                  then g2 = (h9 - ( 0_ (n,L))) by A39, POLYRED: 5

                  .= (Q . k) by A30, POLYRED: 4;

                  hence contradiction by A8, A10, A11, A34, A36;

                end;

                reconsider mp = (m9 *' p9) as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

                reconsider pp = p9 as Element of P by A37;

                set B = (A9 ^ <*mp*>);

                reconsider mm = m9 as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

                

                 A43: gg = (hh - mp) by A39, Lm3;

                reconsider m9 as non-zero Monomial of n, L by A42, POLYNOM7:def 1;

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

                ( len B) = (( len A9) + ( len <*(m9 *' p9)*>)) by FINSEQ_1: 22

                .= (( len A9) + 1) by FINSEQ_1: 40;

                then

                 A44: ( dom B) = ( Seg (( len A9) + 1)) by FINSEQ_1:def 3;

                

                 A45: mp = (mm * pp) by POLYNOM1:def 11;

                now

                  let i be set;

                  assume

                   A46: i in ( dom B);

                  then

                  reconsider j = i as Element of NAT ;

                  

                   A47: j <= (( len A9) + 1) by A44, A46, FINSEQ_1: 1;

                  

                   A48: 1 <= j by A44, A46, FINSEQ_1: 1;

                  now

                    per cases ;

                      case j = (( len A9) + 1);

                      

                      then mp = (B . j) by FINSEQ_1: 42

                      .= (B /. j) by A46, PARTFUN1:def 6;

                      hence ex u be Element of ( Polynom-Ring (n,L)), a be Element of P st (B /. i) = (u * a) by A45;

                    end;

                      case j <> (( len A9) + 1);

                      then j < (( len A9) + 1) by A47, XXREAL_0: 1;

                      then j <= ( len A9) by NAT_1: 13;

                      then j in ( Seg ( len A9)) by A48, FINSEQ_1: 1;

                      then

                       A49: j in ( dom A9) by FINSEQ_1:def 3;

                      then

                      consider m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L such that

                       A50: p in P and

                       A51: (A9 . j) = (m *' p) and ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A32;

                      reconsider a9 = p as Element of P by A50;

                      reconsider u9 = m as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

                      

                       A52: (B . j) = (B /. j) by A46, PARTFUN1:def 6;

                      (u9 * a9) = (m *' p) by POLYNOM1:def 11

                      .= (B /. j) by A49, A51, A52, FINSEQ_1:def 7;

                      hence ex u be Element of ( Polynom-Ring (n,L)), a be Element of P st (B /. i) = (u * a);

                    end;

                  end;

                  hence ex u be Element of ( Polynom-Ring (n,L)), a be Element of P st (B /. i) = (u * a);

                end;

                then

                reconsider B as LeftLinearCombination of P by IDEAL_1:def 9;

                h9 is_reducible_wrt (p9,T) by A38, POLYRED:def 8;

                then h9 <> ( 0_ (n,L)) by POLYRED: 37;

                then ( HT (h9,T)) <= (( HT (f,T)),T) by A35, POLYRED: 44;

                then

                 A53: ( HT ((m9 *' p9),T)) <= (( HT (f,T)),T) by A40, TERMORD: 8;

                 A54:

                now

                  let i be Element of NAT ;

                  assume

                   A55: i in ( dom B);

                  then

                   A56: i <= (( len A9) + 1) by A44, FINSEQ_1: 1;

                  

                   A57: 1 <= i by A44, A55, FINSEQ_1: 1;

                  now

                    per cases ;

                      case i = (( len A9) + 1);

                      hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (B . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A37, A53, FINSEQ_1: 42;

                    end;

                      case i <> (( len A9) + 1);

                      then i < (( len A9) + 1) by A56, XXREAL_0: 1;

                      then i <= ( len A9) by NAT_1: 13;

                      then i in ( Seg ( len A9)) by A57, FINSEQ_1: 1;

                      then

                       A58: i in ( dom A9) by FINSEQ_1:def 3;

                      then

                      consider m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L such that

                       A59: p in P and

                       A60: (A9 . i) = (m *' p) and

                       A61: ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A32;

                      (B . i) = (m *' p) by A58, A60, FINSEQ_1:def 7;

                      hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (B . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A59, A61;

                    end;

                  end;

                  hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (B . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T);

                end;

                take B;

                (gg + ( Sum B)) = (gg + (( Sum A9) + ( Sum <*mp*>))) by RLVECT_1: 41

                .= (gg + (( Sum A9) + mp)) by RLVECT_1: 44

                .= ((hh + ( - mp)) + (( Sum A9) + mp)) by A43

                .= (hh + (( - mp) + (( Sum A9) + mp))) by RLVECT_1:def 3

                .= (hh + (( Sum A9) + (( - mp) + mp))) by RLVECT_1:def 3

                .= (hh + (( Sum A9) + ( 0. ( Polynom-Ring (n,L))))) by RLVECT_1: 5

                .= (hh + ( Sum A9)) by RLVECT_1: 4

                .= f9 by A5, A13, A29, A31, FINSEQ_1: 3, FUNCT_1: 47;

                hence thesis by A8, A10, A11, A36, A54;

              end;

            end;

            hence thesis;

          end;

          hence thesis;

        end;

      end;

      

       A62: P[1]

      proof

        set A = ( <*> the carrier of ( Polynom-Ring (n,L)));

        let f,g be Polynomial of n, L, f9,g9 be Element of ( Polynom-Ring (n,L));

        assume

         A63: f = f9 & g = g9;

        let P be non empty Subset of ( Polynom-Ring (n,L)), R be RedSequence of ( PolyRedRel (P,T));

        for i be set st i in ( dom A) holds ex u be Element of ( Polynom-Ring (n,L)), a be Element of P st (A /. i) = (u * a);

        then

        reconsider A as LeftLinearCombination of P by IDEAL_1:def 9;

        assume

         A64: (R . 1) = f & (R . ( len R)) = g & ( len R) = 1;

        take A;

        f9 = (g9 + ( 0. ( Polynom-Ring (n,L)))) by A63, A64, RLVECT_1:def 4

        .= (g9 + ( Sum A)) by RLVECT_1: 43;

        hence thesis;

      end;

      

       A65: for k be Nat st 1 <= k holds P[k] from NAT_1:sch 8( A62, A4);

      1 <= ( len R) by NAT_1: 14;

      hence thesis by A1, A65, A2;

    end;

    theorem :: GROEB_2:33

    for n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P, b be bag of n st A is_Standard_Representation_of (f,P,b,T) & B is_Standard_Representation_of (g,P,b,T) holds (A ^ B) is_Standard_Representation_of ((f + g),P,b,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P, b be bag of n;

      assume that

       A1: A is_Standard_Representation_of (f,P,b,T) and

       A2: B is_Standard_Representation_of (g,P,b,T);

       A3:

      now

        let i be Element of NAT ;

        assume

         A4: i in ( dom (A ^ B));

        now

          per cases by A4, FINSEQ_1: 25;

            case

             A5: i in ( dom A);

            ((A ^ B) /. i) = ((A ^ B) . i) by A4, PARTFUN1:def 6

            .= (A . i) by A5, FINSEQ_1:def 7

            .= (A /. i) by A5, PARTFUN1:def 6;

            hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & ((A ^ B) /. i) = (m *' p) & ( HT ((m *' p),T)) <= (b,T) by A1, A5;

          end;

            case ex k be Nat st k in ( dom B) & i = (( len A) + k);

            then

            consider k be Nat such that

             A6: k in ( dom B) and

             A7: i = (( len A) + k);

            ((A ^ B) /. i) = ((A ^ B) . i) by A4, PARTFUN1:def 6

            .= (B . k) by A6, A7, FINSEQ_1:def 7

            .= (B /. k) by A6, PARTFUN1:def 6;

            hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & ((A ^ B) /. i) = (m *' p) & ( HT ((m *' p),T)) <= (b,T) by A2, A6;

          end;

        end;

        hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & ((A ^ B) /. i) = (m *' p) & ( HT ((m *' p),T)) <= (b,T);

      end;

      f = ( Sum A) & g = ( Sum B) by A1, A2;

      

      then (f + g) = (( Sum A) + ( Sum B)) by POLYNOM1:def 11

      .= ( Sum (A ^ B)) by RLVECT_1: 41;

      hence thesis by A3;

    end;

    theorem :: GROEB_2:34

    for n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P, b be bag of n, i be Element of NAT st A is_Standard_Representation_of (f,P,b,T) & B = (A | i) & g = ( Sum (A /^ i)) holds B is_Standard_Representation_of ((f - g),P,b,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P, b be bag of n, i be Element of NAT ;

      assume that

       A1: A is_Standard_Representation_of (f,P,b,T) and

       A2: B = (A | i) and

       A3: g = ( Sum (A /^ i));

      

       A4: ( Sum A) = f by A1;

      ( dom (A | ( Seg i))) c= ( dom A) by RELAT_1: 60;

      then

       A5: ( dom B) c= ( dom A) by A2, FINSEQ_1:def 15;

       A6:

      now

        let j be Element of NAT ;

        assume

         A7: j in ( dom B);

        then

         A8: j in ( dom (A | ( Seg i))) by A2, FINSEQ_1:def 15;

        (A /. j) = (A . j) by A5, A7, PARTFUN1:def 6

        .= ((A | ( Seg i)) . j) by A8, FUNCT_1: 47

        .= (B . j) by A2, FINSEQ_1:def 15

        .= (B /. j) by A7, PARTFUN1:def 6;

        hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (B /. j) = (m *' p) & ( HT ((m *' p),T)) <= (b,T) by A1, A5, A7;

      end;

      A = (B ^ (A /^ i)) by A2, RFINSEQ: 8;

      then ( Sum A) = (( Sum B) + ( Sum (A /^ i))) by RLVECT_1: 41;

      

      then (( Sum A) + ( - ( Sum (A /^ i)))) = (( Sum B) + (( Sum (A /^ i)) + ( - ( Sum (A /^ i))))) by RLVECT_1:def 3

      .= (( Sum B) + ( 0. ( Polynom-Ring (n,L)))) by RLVECT_1: 5

      .= ( Sum B) by RLVECT_1:def 4;

      

      then ( Sum B) = (( Sum A) - ( Sum (A /^ i)))

      .= (f - g) by A3, A4, Lm3;

      hence thesis by A6;

    end;

    theorem :: GROEB_2:35

    for n be Ordinal, T be connected TermOrder of n, L be Abelian right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P, b be bag of n, i be Element of NAT st A is_Standard_Representation_of (f,P,b,T) & B = (A /^ i) & g = ( Sum (A | i)) & i <= ( len A) holds B is_Standard_Representation_of ((f - g),P,b,T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be Abelian right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f,g be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A,B be LeftLinearCombination of P, b be bag of n, i be Element of NAT ;

      assume that

       A1: A is_Standard_Representation_of (f,P,b,T) and

       A2: B = (A /^ i) and

       A3: g = ( Sum (A | i)) and

       A4: i <= ( len A);

      

       A5: ( Sum A) = f by A1;

       A6:

      now

        let j be Element of NAT ;

        assume

         A7: j in ( dom B);

        then

         A8: (j + i) in ( dom A) by A2, FINSEQ_5: 26;

        (B /. j) = (B . j) by A7, PARTFUN1:def 6

        .= (A . (j + i)) by A2, A4, A7, RFINSEQ:def 1

        .= (A /. (j + i)) by A8, PARTFUN1:def 6;

        hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (B /. j) = (m *' p) & ( HT ((m *' p),T)) <= (b,T) by A1, A8;

      end;

      A = ((A | i) ^ B) by A2, RFINSEQ: 8;

      then ( Sum A) = (( Sum (A | i)) + ( Sum B)) by RLVECT_1: 41;

      

      then (( Sum A) + ( - ( Sum (A | i)))) = ((( Sum (A | i)) + ( - ( Sum (A | i)))) + ( Sum B)) by RLVECT_1:def 3

      .= (( 0. ( Polynom-Ring (n,L))) + ( Sum B)) by RLVECT_1: 5

      .= ( Sum B) by ALGSTR_1:def 2;

      

      then ( Sum B) = (( Sum A) - ( Sum (A | i)))

      .= (f - g) by A3, A5, Lm3;

      hence thesis by A6;

    end;

    theorem :: GROEB_2:36

    

     Th36: for n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be non-zero Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P st A is_MonomialRepresentation_of f holds ex i be Element of NAT , m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st i in ( dom A) & p in P & (A . i) = (m *' p) & ( HT (f,T)) <= (( HT ((m *' p),T)),T)

    proof

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be non-zero Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P;

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

      then

       A1: (f . ( HT (f,T))) <> ( 0. L) by TERMORD:def 7;

      assume A is_MonomialRepresentation_of f;

      then

      consider i be Element of NAT such that

       A2: i in ( dom A) and

       A3: ex m be Monomial of n, L, p be Polynomial of n, L st (A . i) = (m *' p) & p in P & ((m *' p) . ( HT (f,T))) <> ( 0. L) by A1, Lm4;

      consider m be Monomial of n, L, p be Polynomial of n, L such that

       A4: (A . i) = (m *' p) and

       A5: ((m *' p) . ( HT (f,T))) <> ( 0. L) and

       A6: p in P by A3;

      

       A7: (m *' p) <> ( 0_ (n,L)) by A5, POLYNOM1: 22;

      then

       A8: m <> ( 0_ (n,L)) by POLYRED: 5;

      p <> ( 0_ (n,L)) by A7, POLYNOM1: 28;

      then

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

      reconsider m as non-zero Monomial of n, L by A8, POLYNOM7:def 1;

      ( HT (f,T)) in ( Support (m *' p)) by A5, POLYNOM1:def 4;

      then ( HT (f,T)) <= (( HT ((m *' p),T)),T) by TERMORD:def 6;

      hence thesis by A2, A4, A6;

    end;

    theorem :: GROEB_2:37

    

     Th37: for n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be non-zero Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P st A is_Standard_Representation_of (f,P,T) holds ex i be Element of NAT , m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & i in ( dom A) & (A /. i) = (m *' p) & ( HT (f,T)) = ( HT ((m *' p),T))

    proof

      let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable well-unital distributive non trivial non empty doubleLoopStr, f be non-zero Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)), A be LeftLinearCombination of P;

      assume A is_Standard_Representation_of (f,P,T);

      then

       A1: A is_Standard_Representation_of (f,P,( HT (f,T)),T);

      then

      consider i be Element of NAT , m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L such that

       A2: i in ( dom A) and p in P and

       A3: (A . i) = (m *' p) and

       A4: ( HT (f,T)) <= (( HT ((m *' p),T)),T) by Th32, Th36;

      consider m9 be non-zero Monomial of n, L, p9 be non-zero Polynomial of n, L such that

       A5: p9 in P and

       A6: (A /. i) = (m9 *' p9) and

       A7: ( HT ((m9 *' p9),T)) <= (( HT (f,T)),T) by A1, A2;

      take i, m9, p9;

      (m *' p) = (m9 *' p9) by A2, A3, A6, PARTFUN1:def 6;

      hence thesis by A2, A4, A5, A6, A7, TERMORD: 7;

    end;

    theorem :: GROEB_2:38

    

     Th38: for n be Ordinal, T be admissible connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non degenerated non empty doubleLoopStr, f be Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)) holds ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L))) implies f has_a_Standard_Representation_of (P,T)

    proof

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

      reconsider f9 = f as Element of ( Polynom-Ring (n,L)) by POLYNOM1:def 11;

      

       A1: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      assume ( PolyRedRel (P,T)) reduces (f,( 0_ (n,L)));

      then

      consider A be LeftLinearCombination of P such that

       A2: f9 = (( 0. ( Polynom-Ring (n,L))) + ( Sum A)) and

       A3: for i be Element of NAT st i in ( dom A) holds ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A1, Lm5;

       A4:

      now

        let i be Element of NAT ;

        assume

         A5: i in ( dom A);

        then ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A . i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A3;

        hence ex m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L st p in P & (A /. i) = (m *' p) & ( HT ((m *' p),T)) <= (( HT (f,T)),T) by A5, PARTFUN1:def 6;

      end;

      f = ( Sum A) by A2, RLVECT_1:def 4;

      then A is_Standard_Representation_of (f,P,( HT (f,T)),T) by A4;

      then A is_Standard_Representation_of (f,P,T);

      hence thesis;

    end;

    theorem :: GROEB_2:39

    

     Th39: for n be Ordinal, T be admissible 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 non-zero Polynomial of n, L, P be non empty Subset of ( Polynom-Ring (n,L)) holds f has_a_Standard_Representation_of (P,T) implies f is_top_reducible_wrt (P,T)

    proof

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

      assume f has_a_Standard_Representation_of (P,T);

      then

      consider A be LeftLinearCombination of P such that

       A1: A is_Standard_Representation_of (f,P,T);

      consider i be Element of NAT , m be non-zero Monomial of n, L, p be non-zero Polynomial of n, L such that

       A2: p in P and i in ( dom A) and (A /. i) = (m *' p) and

       A3: ( HT (f,T)) = ( HT ((m *' p),T)) by A1, Th37;

      set s = ( HT (m,T));

      

       A4: ( HT (f,T)) = (s + ( HT (p,T))) by A3, TERMORD: 31;

      set g = (f - (((f . ( HT (f,T))) / ( HC (p,T))) * (s *' p)));

      

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

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

      then p <> ( 0_ (n,L)) & ( HT (f,T)) in ( Support f) by POLYNOM7:def 1, TERMORD:def 6;

      then f reduces_to (g,p,( HT (f,T)),T) by A5, A4, POLYRED:def 5;

      then f top_reduces_to (g,p,T) by POLYRED:def 10;

      then f is_top_reducible_wrt (p,T) by POLYRED:def 11;

      hence thesis by A2, POLYRED:def 12;

    end;

    theorem :: GROEB_2:40

    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 non empty Subset of ( Polynom-Ring (n,L)) holds G is_Groebner_basis_wrt T iff for f be non-zero Polynomial of n, L st f in (G -Ideal ) holds f has_a_Standard_Representation_of (G,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, P be non empty Subset of ( Polynom-Ring (n,L));

       A1:

      now

        assume for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f has_a_Standard_Representation_of (P,T);

        then for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f is_top_reducible_wrt (P,T) by Th39;

        then for b be bag of n st b in ( HT ((P -Ideal ),T)) holds ex b9 be bag of n st b9 in ( HT (P,T)) & b9 divides b by GROEB_1: 18;

        then ( HT ((P -Ideal ),T)) c= ( multiples ( HT (P,T))) by GROEB_1: 19;

        then ( PolyRedRel (P,T)) is locally-confluent by GROEB_1: 20;

        hence P is_Groebner_basis_wrt T by GROEB_1:def 3;

      end;

      

       A2: ( 0_ (n,L)) = ( 0. ( Polynom-Ring (n,L))) by POLYNOM1:def 11;

      now

        assume P is_Groebner_basis_wrt T;

        then ( PolyRedRel (P,T)) is locally-confluent by GROEB_1:def 3;

        hence for f be non-zero Polynomial of n, L st f in (P -Ideal ) holds f has_a_Standard_Representation_of (P,T) by A2, Th38, GROEB_1: 15;

      end;

      hence thesis by A1;

    end;