let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds
for m1, m2 being 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 ) holds
P is_Groebner_basis_wrt T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L) st ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds
for m1, m2 being 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 ) holds
P is_Groebner_basis_wrt T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring n,L) st ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds
for m1, m2 being 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 ) holds
P is_Groebner_basis_wrt T
let P be Subset of (Polynom-Ring n,L); :: thesis: ( ( for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds
for m1, m2 being 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 )
assume A1: for p1, p2 being Polynomial of n,L st p1 <> p2 & p1 in P & p2 in P holds
for m1, m2 being 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 ; :: thesis: P is_Groebner_basis_wrt T
set R = PolyRedRel P,T;
A2: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;

now

let a, b, c be set ; :: thesis: ( [a,b] in PolyRedRel P,T & [a,c] in PolyRedRel P,T implies b,c are_convergent_wrt PolyRedRel P,T )
assume that
A3: [a,b] in PolyRedRel P,T and
A4: [a,c] in PolyRedRel P,T ; :: thesis: b,c are_convergent_wrt PolyRedRel P,T
consider f, f1 being set 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 = f as Polynomial of n,L by A5, POLYNOM1:def 27;
f <> 0_ n,L by A8, TARSKI:def 1;
then reconsider f = f as non-zero Polynomial of n,L by POLYNOM7:def 2;
reconsider f1 = f1 as Polynomial of n,L by A6, POLYNOM1:def 27;
f reduces_to f1,P,T by A3, A7, POLYRED:def 13;
then consider g1 being Polynomial of n,L such that
A9: g1 in P and
A10: f reduces_to f1,g1,T by POLYRED:def 7;
ex b1 being 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 being set 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 = f2 as Polynomial of n,L by A12, POLYNOM1:def 27;
A14: f2 = [a,c] `2 by A13, MCART_1:def 2
.= c by MCART_1:def 2 ;
reconsider g1 = g1 as non-zero Polynomial of n,L by A11, POLYNOM7:def 2;
consider m1 being 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,c] `1 by A13, MCART_1:def 1
.= a by MCART_1:def 1 ;
A18: f9 = [a,c] `1 by A13, MCART_1:def 1
.= a by MCART_1:def 1
.= [f,f1] `1 by A7, MCART_1:def 1
.= f by MCART_1:def 1 ;
then f reduces_to f2,P,T by A4, A13, POLYRED:def 13;
then consider g2 being Polynomial of n,L such that
A19: g2 in P and
A20: f reduces_to f2,g2,T by POLYRED:def 7;
ex b2 being 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 = g2 as non-zero Polynomial of n,L by POLYNOM7:def 2;
consider m2 being 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;
set mg2 = m2 *' g2;
A24: f1 = [a,b] `2 by A7, MCART_1:def 2
.= b by MCART_1:def 2 ;

now

per cases ( m1 = 0_ n,L or m2 = 0_ n,L or ( m1 <> 0_ n,L & m2 <> 0_ n,L ) ) ;

case m1 = 0_ n,L ; :: thesis: b,c are_convergent_wrt PolyRedRel P,T

then f1 = f - (0_ n,L) by A15, POLYRED:5
.= f by POLYRED:4 ;
then A25: PolyRedRel P,T reduces b,c by A4, A18, A24, A17, REWRITE1:16;
PolyRedRel P,T reduces c,c by REWRITE1:13;
hence b,c are_convergent_wrt PolyRedRel P,T by A25, REWRITE1:def 7; :: thesis: verum

end;

case m2 = 0_ n,L ; :: thesis: b,c are_convergent_wrt PolyRedRel P,T

then f2 = f - (0_ n,L) by A22, POLYRED:5
.= f by POLYRED:4 ;
then A26: PolyRedRel P,T reduces c,b by A3, A18, A14, A17, REWRITE1:16;
PolyRedRel P,T reduces b,b by REWRITE1:13;
hence b,c are_convergent_wrt PolyRedRel P,T by A26, REWRITE1:def 7; :: thesis: verum

end;

case ( m1 <> 0_ n,L & m2 <> 0_ n,L ) ; :: thesis: b,c are_convergent_wrt PolyRedRel P,T

then reconsider m1 = m1, m2 = m2 as non-zero Monomial of n,L by POLYNOM7:def 2;
(HT m1,T) + (HT g1,T) in Support (m1 *' g1) by TERMORD:29;
then A27: m1 *' g1 <> 0_ n,L by POLYNOM7:1;
(HT m2,T) + (HT g2,T) in Support (m2 *' g2) by TERMORD:29;
then A28: m2 *' g2 <> 0_ n,L by POLYNOM7:1;
A29: HC g2,T <> 0. L ;
A30: f2 - f1 = (f + (- (m2 *' g2))) - (f - (m1 *' g1)) by A15, A22, POLYNOM1:def 23
.= (f + (- (m2 *' g2))) - (f + (- (m1 *' g1))) by POLYNOM1:def 23
.= (f + (- (m2 *' g2))) + (- (f + (- (m1 *' g1)))) by POLYNOM1:def 23
.= (f + (- (m2 *' g2))) + ((- f) + (- (- (m1 *' g1)))) by POLYRED:1
.= f + ((- (m2 *' g2)) + ((- f) + (m1 *' g1))) by POLYNOM1:80
.= f + ((- f) + ((- (m2 *' g2)) + (m1 *' g1))) by POLYNOM1:80
.= (f + (- f)) + ((- (m2 *' g2)) + (m1 *' g1)) by POLYNOM1:80
.= (0_ n,L) + ((- (m2 *' g2)) + (m1 *' g1)) by POLYRED:3
.= (m1 *' g1) + (- (m2 *' g2)) by POLYRED:2
.= (m1 *' g1) - (m2 *' g2) by POLYNOM1:def 23 ;
A31: HC g1,T <> 0. L ;
PolyRedRel P,T reduces f2 - f1, 0_ n,L

proof

now

per cases ( (m1 *' g1) - (m2 *' g2) = 0_ n,L or (m1 *' g1) - (m2 *' g2) <> 0_ n,L ) ;

case (m1 *' g1) - (m2 *' g2) = 0_ n,L ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

hence PolyRedRel P,T reduces f2 - f1, 0_ n,L by A30, REWRITE1:13; :: thesis: verum

end;

case A32: (m1 *' g1) - (m2 *' g2) <> 0_ n,L ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

now

per cases ( g1 = g2 or g1 <> g2 ) ;

case g1 = g2 ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

then f2 - f1 = (m1 *' g1) + (- (m2 *' g1)) by A30, POLYNOM1:def 23
.= (g1 *' m1) + ((- m2) *' g1) by POLYRED:6
.= (m1 + (- m2)) *' g1 by POLYNOM1:85 ;
hence PolyRedRel P,T reduces f2 - f1, 0_ n,L by A9, POLYRED:45; :: thesis: verum

end;

case A33: g1 <> g2 ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

now

per cases ( HT (m1 *' g1),T <> HT (m2 *' g2),T or HT (m1 *' g1),T = HT (m2 *' g2),T ) ;

case A34: HT (m1 *' g1),T <> HT (m2 *' g2),T ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

now

per cases ( HT (m2 *' g2),T < HT (m1 *' g1),T,T or not HT (m2 *' g2),T < HT (m1 *' g1),T,T ) ;

case HT (m2 *' g2),T < HT (m1 *' g1),T,T ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

then not HT (m1 *' g1),T <= HT (m2 *' g2),T,T by TERMORD:5;
then not HT (m1 *' g1),T in Support (m2 *' g2) by TERMORD:def 6;
then A35: (m2 *' g2) . (HT (m1 *' g1),T) = 0. L by POLYNOM1:def 9;
A36: ((m1 *' g1) - (m2 *' g2)) . (HT (m1 *' g1),T) = ((m1 *' g1) + (- (m2 *' g2))) . (HT (m1 *' g1),T) by POLYNOM1:def 23
.= ((m1 *' g1) . (HT (m1 *' g1),T)) + ((- (m2 *' g2)) . (HT (m1 *' g1),T)) by POLYNOM1:def 21
.= ((m1 *' g1) . (HT (m1 *' g1),T)) + (- ((m2 *' g2) . (HT (m1 *' g1),T))) by POLYNOM1:def 22
.= ((m1 *' g1) . (HT (m1 *' g1),T)) + (0. L) by A35, RLVECT_1:25
.= (m1 *' g1) . (HT (m1 *' g1),T) by RLVECT_1:def 7
.= HC (m1 *' g1),T by TERMORD:def 7 ;
then ((m1 *' g1) - (m2 *' g2)) . (HT (m1 *' g1),T) <> 0. L by A27, TERMORD:17;
then A37: HT (m1 *' g1),T in Support ((m1 *' g1) - (m2 *' g2)) by POLYNOM1:def 9;
A38: (HT m1,T) + (HT g1,T) = HT (m1 *' g1),T by TERMORD:31;
((m1 *' g1) - (m2 *' g2)) - (((((m1 *' g1) - (m2 *' g2)) . (HT (m1 *' g1),T)) / (HC g1,T)) * ((HT m1,T) *' g1)) = ((m1 *' g1) - (m2 *' g2)) - ((((HC m1,T) * (HC g1,T)) / (HC g1,T)) * ((HT m1,T) *' g1)) by A36, TERMORD:32
.= ((m1 *' g1) - (m2 *' g2)) - ((((HC m1,T) * (HC g1,T)) * ((HC g1,T) " )) * ((HT m1,T) *' g1)) by VECTSP_1:def 23
.= ((m1 *' g1) - (m2 *' g2)) - (((HC m1,T) * ((HC g1,T) * ((HC g1,T) " ))) * ((HT m1,T) *' g1)) by GROUP_1:def 4
.= ((m1 *' g1) - (m2 *' g2)) - (((HC m1,T) * (1. L)) * ((HT m1,T) *' g1)) by A31, VECTSP_1:def 22
.= ((m1 *' g1) - (m2 *' g2)) - ((HC m1,T) * ((HT m1,T) *' g1)) by VECTSP_1:def 19
.= ((m1 *' g1) - (m2 *' g2)) - ((Monom (HC m1,T),(HT m1,T)) *' g1) by POLYRED:22
.= ((m1 *' g1) - (m2 *' g2)) - ((Monom (coefficient m1),(HT m1,T)) *' g1) by TERMORD:23
.= ((m1 *' g1) - (m2 *' g2)) - ((Monom (coefficient m1),(term m1)) *' g1) by TERMORD:23
.= ((m1 *' g1) - (m2 *' g2)) - (m1 *' g1) by POLYNOM7:11
.= ((m1 *' g1) + (- (m2 *' g2))) - (m1 *' g1) by POLYNOM1:def 23
.= ((m1 *' g1) + (- (m2 *' g2))) + (- (m1 *' g1)) by POLYNOM1:def 23
.= ((m1 *' g1) + (- (m1 *' g1))) + (- (m2 *' g2)) by POLYNOM1:80
.= (0_ n,L) + (- (m2 *' g2)) by POLYRED:3
.= - (m2 *' g2) by POLYRED:2 ;
then (m1 *' g1) - (m2 *' g2) reduces_to - (m2 *' g2),g1, HT (m1 *' g1),T,T by A11, A32, A37, A38, POLYRED:def 5;
then (m1 *' g1) - (m2 *' g2) reduces_to - (m2 *' g2),g1,T by POLYRED:def 6;
then (m1 *' g1) - (m2 *' g2) reduces_to - (m2 *' g2),P,T by A9, POLYRED:def 7;
then [((m1 *' g1) - (m2 *' g2)),(- (m2 *' g2))] in PolyRedRel P,T by POLYRED:def 13;
then A39: PolyRedRel P,T reduces (m1 *' g1) - (m2 *' g2), - (m2 *' g2) by REWRITE1:16;
PolyRedRel P,T reduces (- m2) *' g2, 0_ n,L by A19, POLYRED:45;
then PolyRedRel P,T reduces - (m2 *' g2), 0_ n,L by POLYRED:6;
hence PolyRedRel P,T reduces f2 - f1, 0_ n,L by A30, A39, REWRITE1:17; :: thesis: verum

end;

case not HT (m2 *' g2),T < HT (m1 *' g1),T,T ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

then HT (m1 *' g1),T <= HT (m2 *' g2),T,T by TERMORD:5;
then HT (m1 *' g1),T < HT (m2 *' g2),T,T by A34, TERMORD:def 3;
then not HT (m2 *' g2),T <= HT (m1 *' g1),T,T by TERMORD:5;
then not HT (m2 *' g2),T in Support (m1 *' g1) by TERMORD:def 6;
then A40: (m1 *' g1) . (HT (m2 *' g2),T) = 0. L by POLYNOM1:def 9;
A41: ((m2 *' g2) - (m1 *' g1)) . (HT (m2 *' g2),T) = ((m2 *' g2) + (- (m1 *' g1))) . (HT (m2 *' g2),T) by POLYNOM1:def 23
.= ((m2 *' g2) . (HT (m2 *' g2),T)) + ((- (m1 *' g1)) . (HT (m2 *' g2),T)) by POLYNOM1:def 21
.= ((m2 *' g2) . (HT (m2 *' g2),T)) + (- ((m1 *' g1) . (HT (m2 *' g2),T))) by POLYNOM1:def 22
.= ((m2 *' g2) . (HT (m2 *' g2),T)) + (0. L) by A40, RLVECT_1:25
.= (m2 *' g2) . (HT (m2 *' g2),T) by RLVECT_1:def 7
.= HC (m2 *' g2),T by TERMORD:def 7 ;
then ((m2 *' g2) - (m1 *' g1)) . (HT (m2 *' g2),T) <> 0. L by A28, TERMORD:17;
then A42: HT (m2 *' g2),T in Support ((m2 *' g2) - (m1 *' g1)) by POLYNOM1:def 9;
reconsider x = - (0_ n,L) as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
A43: (HT m2,T) + (HT g2,T) = HT (m2 *' g2),T by TERMORD:31;
reconsider x = x as Element of (Polynom-Ring n,L) ;
0. (Polynom-Ring n,L) = 0_ n,L by POLYNOM1:def 27;
then A44: x + (0. (Polynom-Ring n,L)) = (- (0_ n,L)) + (0_ n,L) by POLYNOM1:def 27
.= 0_ n,L by POLYRED:3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;

A45: now

assume (m2 *' g2) - (m1 *' g1) = 0_ n,L ; :: thesis: contradiction
then - ((m2 *' g2) + (- (m1 *' g1))) = - (0_ n,L) by POLYNOM1:def 23;
then (- (m2 *' g2)) + (- (- (m1 *' g1))) = - (0_ n,L) by POLYRED:1;
then (m1 *' g1) + (- (m2 *' g2)) = - (0. (Polynom-Ring n,L)) by A44, RLVECT_1:19
.= 0. (Polynom-Ring n,L) by RLVECT_1:25
.= 0_ n,L by POLYNOM1:def 27 ;
hence contradiction by A32, POLYNOM1:def 23; :: thesis: verum

end;

((m2 *' g2) - (m1 *' g1)) - (((((m2 *' g2) - (m1 *' g1)) . (HT (m2 *' g2),T)) / (HC g2,T)) * ((HT m2,T) *' g2)) = ((m2 *' g2) - (m1 *' g1)) - ((((HC m2,T) * (HC g2,T)) / (HC g2,T)) * ((HT m2,T) *' g2)) by A41, TERMORD:32
.= ((m2 *' g2) - (m1 *' g1)) - ((((HC m2,T) * (HC g2,T)) * ((HC g2,T) " )) * ((HT m2,T) *' g2)) by VECTSP_1:def 23
.= ((m2 *' g2) - (m1 *' g1)) - (((HC m2,T) * ((HC g2,T) * ((HC g2,T) " ))) * ((HT m2,T) *' g2)) by GROUP_1:def 4
.= ((m2 *' g2) - (m1 *' g1)) - (((HC m2,T) * (1. L)) * ((HT m2,T) *' g2)) by A29, VECTSP_1:def 22
.= ((m2 *' g2) - (m1 *' g1)) - ((HC m2,T) * ((HT m2,T) *' g2)) by VECTSP_1:def 19
.= ((m2 *' g2) - (m1 *' g1)) - ((Monom (HC m2,T),(HT m2,T)) *' g2) by POLYRED:22
.= ((m2 *' g2) - (m1 *' g1)) - ((Monom (coefficient m2),(HT m2,T)) *' g2) by TERMORD:23
.= ((m2 *' g2) - (m1 *' g1)) - ((Monom (coefficient m2),(term m2)) *' g2) by TERMORD:23
.= ((m2 *' g2) - (m1 *' g1)) - (m2 *' g2) by POLYNOM7:11
.= ((m2 *' g2) + (- (m1 *' g1))) - (m2 *' g2) by POLYNOM1:def 23
.= ((m2 *' g2) + (- (m1 *' g1))) + (- (m2 *' g2)) by POLYNOM1:def 23
.= ((m2 *' g2) + (- (m2 *' g2))) + (- (m1 *' g1)) by POLYNOM1:80
.= (0_ n,L) + (- (m1 *' g1)) by POLYRED:3
.= - (m1 *' g1) by POLYRED:2 ;
then (m2 *' g2) - (m1 *' g1) reduces_to - (m1 *' g1),g2, HT (m2 *' g2),T,T by A21, A42, A43, A45, POLYRED:def 5;
then (m2 *' g2) - (m1 *' g1) reduces_to - (m1 *' g1),g2,T by POLYRED:def 6;
then (m2 *' g2) - (m1 *' g1) reduces_to - (m1 *' g1),P,T by A19, POLYRED:def 7;
then [((m2 *' g2) - (m1 *' g1)),(- (m1 *' g1))] in PolyRedRel P,T by POLYRED:def 13;
then A46: PolyRedRel P,T reduces (m2 *' g2) - (m1 *' g1), - (m1 *' g1) by REWRITE1:16;
A47: - (1_ n,L) = - ((1. L) | n,L) by POLYNOM7:20
.= (- (1. L)) | n,L by Th20 ;
PolyRedRel P,T reduces (- m1) *' g1, 0_ n,L by A9, POLYRED:45;
then PolyRedRel P,T reduces - (m1 *' g1), 0_ n,L by POLYRED:6;
then PolyRedRel P,T reduces (m2 *' g2) - (m1 *' g1), 0_ n,L by A46, REWRITE1:17;
then A48: PolyRedRel P,T reduces (- (1_ n,L)) *' ((m2 *' g2) - (m1 *' g1)),(- (1_ n,L)) *' (0_ n,L) by A47, POLYRED:47;
(- (1_ n,L)) *' ((m2 *' g2) - (m1 *' g1)) = (- (1_ n,L)) *' ((m2 *' g2) + (- (m1 *' g1))) by POLYNOM1:def 23
.= ((- (1_ n,L)) *' (m2 *' g2)) + ((- (1_ n,L)) *' (- (m1 *' g1))) by POLYNOM1:85
.= (- ((1_ n,L) *' (m2 *' g2))) + ((- (1_ n,L)) *' (- (m1 *' g1))) by POLYRED:6
.= ((1_ n,L) *' (- (m2 *' g2))) + ((- (1_ n,L)) *' (- (m1 *' g1))) by POLYRED:6
.= ((1_ n,L) *' (- (m2 *' g2))) + (- ((1_ n,L) *' (- (m1 *' g1)))) by POLYRED:6
.= ((1_ n,L) *' (- (m2 *' g2))) + ((1_ n,L) *' (- (- (m1 *' g1)))) by POLYRED:6
.= (- (m2 *' g2)) + ((1_ n,L) *' (m1 *' g1)) by POLYNOM1:89
.= (m1 *' g1) + (- (m2 *' g2)) by POLYNOM1:89
.= (m1 *' g1) - (m2 *' g2) by POLYNOM1:def 23 ;
hence PolyRedRel P,T reduces f2 - f1, 0_ n,L by A30, A48, POLYNOM1:87; :: thesis: verum

end;

end;

end;

hence PolyRedRel P,T reduces f2 - f1, 0_ n,L ; :: thesis: verum

end;

case A49: HT (m1 *' g1),T = HT (m2 *' g2),T ; :: thesis: PolyRedRel P,T reduces f2 - f1, 0_ n,L

(f - (m2 *' g2)) . (HT (m2 *' g2),T) = 0. L by A22, A23, POLYNOM1:def 9;
then (f + (- (m2 *' g2))) . (HT (m2 *' g2),T) = 0. L by POLYNOM1:def 23;
then (f . (HT (m2 *' g2),T)) + ((- (m2 *' g2)) . (HT (m2 *' g2),T)) = 0. L by POLYNOM1:def 21;
then (f . (HT (m2 *' g2),T)) + (- ((m2 *' g2) . (HT (m2 *' g2),T))) = 0. L by POLYNOM1:def 22;
then A50: f . (HT (m2 *' g2),T) = - (- ((m2 *' g2) . (HT (m2 *' g2),T))) by RLVECT_1:19;
(f - (m1 *' g1)) . (HT (m1 *' g1),T) = 0. L by A15, A16, POLYNOM1:def 9;
then (f + (- (m1 *' g1))) . (HT (m1 *' g1),T) = 0. L by POLYNOM1:def 23;
then (f . (HT (m1 *' g1),T)) + ((- (m1 *' g1)) . (HT (m1 *' g1),T)) = 0. L by POLYNOM1:def 21;
then (f . (HT (m1 *' g1),T)) + (- ((m1 *' g1) . (HT (m1 *' g1),T))) = 0. L by POLYNOM1:def 22;
then A51: f . (HT (m1 *' g1),T) = - (- ((m1 *' g1) . (HT (m1 *' g1),T))) by RLVECT_1:19;
HC (m1 *' g1),T = (m1 *' g1) . (HT (m1 *' g1),T) by TERMORD:def 7
.= f . (HT (m1 *' g1),T) by A51, RLVECT_1:30
.= (m2 *' g2) . (HT (m2 *' g2),T) by A49, A50, RLVECT_1:30
.= HC (m2 *' g2),T by TERMORD:def 7 ;
then HM (m1 *' g1),T = Monom (HC (m2 *' g2),T),(HT (m2 *' g2),T) by A49, TERMORD:def 8
.= HM (m2 *' g2),T by TERMORD:def 8 ;
hence PolyRedRel P,T reduces f2 - f1, 0_ n,L by A1, A9, A19, A30, A33; :: thesis: verum

end;

end;

end;

hence PolyRedRel P,T reduces f2 - f1, 0_ n,L ; :: thesis: verum

end;

end;

end;

hence PolyRedRel P,T reduces f2 - f1, 0_ n,L ; :: thesis: verum

end;

end;

end;

hence PolyRedRel P,T reduces f2 - f1, 0_ n,L ; :: thesis: verum

end;

hence b,c are_convergent_wrt PolyRedRel P,T by A24, A14, POLYRED:50, REWRITE1:41; :: thesis: verum

end;

end;

end;

hence b,c are_convergent_wrt PolyRedRel P,T ; :: thesis: verum

end;

then PolyRedRel P,T is locally-confluent by REWRITE1:def 24;
hence P is_Groebner_basis_wrt T by GROEB_1:def 3; :: thesis: verum