let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis:
let G, H be non empty finite Subset of (Polynom-Ring (n,L)); :: thesis:
assume that
A1: G is_Groebner_basis_of I,T and
A2: G is_reduced_wrt T and
A3: H is_Groebner_basis_of I,T and
A4: H is_reduced_wrt T ; :: thesis:
A5: H -Ideal = I by A3;
set GH = (G \/ H) \ (G /\ H);
assume A6: G <> H ; :: thesis:

now :: thesis:

assume (G \/ H) \ (G /\ H) = {} ; :: thesis:
then A7: G \/ H c= G /\ H by XBOOLE_1:37;

A8: now :: thesis:

let u be object ; :: thesis:
assume u in H ; :: thesis:
then u in G \/ H by XBOOLE_0:def 3;
hence u in G by A7, XBOOLE_0:def 4; :: thesis:

end;

now :: thesis:

let u be object ; :: thesis:
assume u in G ; :: thesis:
then u in G \/ H by XBOOLE_0:def 3;
hence u in H by A7, XBOOLE_0:def 4; :: thesis:

end;

hence contradiction by A6, A8, TARSKI:2; :: thesis:

end;

then reconsider GH = (G \/ H) \ (G /\ H) as non empty Subset of (Polynom-Ring (n,L)) ;

A9: now :: thesis:

let u be object ; :: thesis:
assume A10: u in GH ; :: thesis:
then A11: not u in G /\ H by XBOOLE_0:def 5;
A12: u in G \/ H by A10, XBOOLE_0:def 5;
( u in G \ H or u in H \ G )

proof

assume A13: not u in G \ H ; :: thesis:

now :: thesis:

per cases by A13, XBOOLE_0:def 5;

case not u in G ; :: thesis:

hence ( not u in G & u in H ) by A12, XBOOLE_0:def 3; :: thesis:

end;

case u in H ; :: thesis:

hence ( u in H & not u in G ) by A11, XBOOLE_0:def 4; :: thesis:

end;

hence u in H \ G by XBOOLE_0:def 5; :: thesis:

end;

hence u in (G \ H) \/ (H \ G) by XBOOLE_0:def 3; :: thesis:

end;

consider g being Polynomial of n,L such that
A14: g in GH and
A15: for q being Polynomial of n,L st q in GH holds
g <= q,T by POLYRED:31;
A16: G -Ideal = I by A1;

A17: now :: thesis:

let u be set ; :: thesis:
assume A18: ( u in G or u in H ) ; :: thesis:

now :: thesis:

per cases by A18;

case A19: u in G ; :: thesis:

then reconsider u9 = u as Element of (Polynom-Ring (n,L)) ;
reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;
u9 is_monic_wrt T by A2, A19;
then A20: HC (u9,T) = 1. L ;
1. L <> 0. L ;
hence ( u is Polynomial of n,L & u <> 0_ (n,L) ) by A20, TERMORD:17; :: thesis:

end;

case A21: u in H ; :: thesis:

then reconsider u9 = u as Element of (Polynom-Ring (n,L)) ;
reconsider u9 = u9 as Polynomial of n,L by POLYNOM1:def 11;
u9 is_monic_wrt T by A4, A21;
then A22: HC (u9,T) = 1. L ;
1. L <> 0. L ;
hence ( u is Polynomial of n,L & u <> 0_ (n,L) ) by A22, TERMORD:17; :: thesis:

end;

hence ( u is Polynomial of n,L & u <> 0_ (n,L) ) ; :: thesis:

end;

PolyRedRel (G,T) is locally-confluent by A1;
then for f being Polynomial of n,L st f in G -Ideal holds
PolyRedRel (G,T) reduces f, 0_ (n,L) by Th15;
then for f being non-zero Polynomial of n,L st f in G -Ideal holds
f is_reducible_wrt G,T by Th16;
then A23: for f being non-zero Polynomial of n,L st f in G -Ideal holds
f is_top_reducible_wrt G,T by Th17;
A24: for u being Polynomial of n,L st ( u in G or u in H ) holds
HC (u,T) = 1. L by Def6, A2, A4;

A25: now :: thesis:

let u be set ; :: thesis:
assume A26: u in GH ; :: thesis:
then not u in G /\ H by XBOOLE_0:def 5;
then A27: ( not u in G or not u in H ) by XBOOLE_0:def 4;
A28: u in G \/ H by A26, XBOOLE_0:def 5;

now :: thesis:

per cases by A28, XBOOLE_0:def 3;

case u in G ; :: thesis:

hence u in G \ H by A27, XBOOLE_0:def 5; :: thesis:

end;

case u in H ; :: thesis:

hence u in H \ G by A27, XBOOLE_0:def 5; :: thesis:

end;

hence ( u in G \ H or u in H \ G ) ; :: thesis:

end;

now :: thesis:

let u be object ; :: thesis:
assume A29: u in (G \ H) \/ (H \ G) ; :: thesis:

now :: thesis:

per cases by A29, XBOOLE_0:def 3;

case u in G \ H ; :: thesis:

then ( u in G & not u in H ) by XBOOLE_0:def 5;
hence ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis:

end;

case u in H \ G ; :: thesis:

then ( u in H & not u in G ) by XBOOLE_0:def 5;
hence ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 3, XBOOLE_0:def 4; :: thesis:

end;

hence u in GH by XBOOLE_0:def 5; :: thesis:

end;

then A30: GH = (G \ H) \/ (H \ G) by A9, TARSKI:2;
PolyRedRel (H,T) is locally-confluent by A3;
then for f being Polynomial of n,L st f in H -Ideal holds
PolyRedRel (H,T) reduces f, 0_ (n,L) by Th15;
then for f being non-zero Polynomial of n,L st f in H -Ideal holds
f is_reducible_wrt H,T by Th16;
then A31: for f being non-zero Polynomial of n,L st f in H -Ideal holds
f is_top_reducible_wrt H,T by Th17;

per cases by A25, A14;

suppose A32: g in G \ H ; :: thesis:

then A33: g in G by XBOOLE_0:def 5;
then A34: g <> 0_ (n,L) by A17;
then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 1;
A35: G c= G -Ideal by IDEAL_1:def 14;
then HT (g,T) in HT ((H -Ideal),T) by A16, A5, A33, A34;
then consider b9 being bag of n such that
A36: b9 in HT (H,T) and
A37: b9 divides HT (g,T) by A31, Th18;
consider h being Polynomial of n,L such that
A38: b9 = HT (h,T) and
A39: h in H and
A40: h <> 0_ (n,L) by A36;
reconsider h = h as non-zero Polynomial of n,L by A40, POLYNOM7:def 1;
set f = g - h;
A41: h <> g by A32, A39, XBOOLE_0:def 5;

A42: now :: thesis:

assume A43: g - h = 0_ (n,L) ; :: thesis:
h = (0_ (n,L)) + h by POLYRED:2
.= (g + (- h)) + h by A43, POLYNOM1:def 7
.= g + ((- h) + h) by POLYNOM1:21
.= g + (0_ (n,L)) by POLYRED:3 ;
hence contradiction by A41, POLYNOM1:23; :: thesis:

end;

Support g <> {} by A34, POLYNOM7:1;
then HT (g,T) in Support g by TERMORD:def 6;
then A44: g is_reducible_wrt h,T by A37, A38, POLYRED:36;
then A45: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;

now :: thesis:

assume not h in H \ G ; :: thesis:
then A46: h in G by A39, XBOOLE_0:def 5;
not h in {g} by A41, TARSKI:def 1;
then h in G \ {g} by A46, XBOOLE_0:def 5;
then consider r being Polynomial of n,L such that
A47: ( h in G \ {g} & g reduces_to r,h,T ) by A45;
A48: g reduces_to r,G \ {g},T by A47, POLYRED:def 7;
g is_irreducible_wrt G \ {g},T by A2, A33;
hence contradiction by A48, POLYRED:def 9; :: thesis:

end;

then h in GH by A30, XBOOLE_0:def 3;
then g <= h,T by A15;
then not h < g,T by POLYRED:29;
then not HT (h,T) < HT (g,T),T by POLYRED:32;
then A49: HT (g,T) <= HT (h,T),T by TERMORD:5;
HT (h,T) <= HT (g,T),T by A44, Th9;
then A50: HT (h,T) = HT (g,T) by A49, TERMORD:7;
reconsider f = g - h as non-zero Polynomial of n,L by A42, POLYNOM7:def 1;
Support f <> {} by A42, POLYNOM7:1;
then A51: HT (f,T) in Support f by TERMORD:def 6;
f . (HT (g,T)) = (g + (- h)) . (HT (g,T)) by POLYNOM1:def 7
.= (g . (HT (g,T))) + ((- h) . (HT (g,T))) by POLYNOM1:15
.= (g . (HT (g,T))) + (- (h . (HT (h,T)))) by A50, POLYNOM1:17
.= (HC (g,T)) + (- (h . (HT (h,T)))) by TERMORD:def 7
.= (HC (g,T)) + (- (HC (h,T))) by TERMORD:def 7
.= (1. L) + (- (HC (h,T))) by A24, A33
.= (1. L) + (- (1. L)) by A24, A39
.= 0. L by RLVECT_1:5 ;
then A52: HT (f,T) <> HT (g,T) by A51, POLYNOM1:def 4;
HT (f,T) <= max ((HT (g,T)),(HT (h,T)),T),T by Th7;
then A53: HT (f,T) <= HT (g,T),T by A50, TERMORD:12;
reconsider g9 = g, h9 = h as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring (n,L)) ;
H c= H -Ideal by IDEAL_1:def 14;
then g9 - h9 in I by A16, A5, A33, A35, A39, IDEAL_1:15;
then f in I by Lm2;
then A54: HT (f,T) in HT (I,T) by A42;
Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:20;
then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 7;
then A55: Support f c= (Support g) \/ (Support h) by Th5;

now :: thesis:

per cases by A51, A55, XBOOLE_0:def 3;

case A56: HT (f,T) in Support g ; :: thesis:

consider b9 being bag of n such that
A57: b9 in HT (G,T) and
A58: b9 divides HT (f,T) by A16, A23, A54, Th18;
consider q being Polynomial of n,L such that
A59: b9 = HT (q,T) and
A60: q in G and
A61: q <> 0_ (n,L) by A57;
reconsider q = q as non-zero Polynomial of n,L by A61, POLYNOM7:def 1;
g is_reducible_wrt q,T by A56, A58, A59, POLYRED:36;
then consider r being Polynomial of n,L such that
A62: g reduces_to r,q,T by POLYRED:def 8;
HT (q,T) <= HT (f,T),T by A58, A59, TERMORD:10;
then q <> g by A53, A52, TERMORD:7;
then not q in {g} by TARSKI:def 1;
then q in G \ {g} by A60, XBOOLE_0:def 5;
then g reduces_to r,G \ {g},T by A62, POLYRED:def 7;
then g is_reducible_wrt G \ {g},T by POLYRED:def 9;
hence contradiction by A2, A33; :: thesis:

end;

case A63: HT (f,T) in Support h ; :: thesis:

consider b9 being bag of n such that
A64: b9 in HT (H,T) and
A65: b9 divides HT (f,T) by A5, A31, A54, Th18;
consider q being Polynomial of n,L such that
A66: b9 = HT (q,T) and
A67: q in H and
A68: q <> 0_ (n,L) by A64;
reconsider q = q as non-zero Polynomial of n,L by A68, POLYNOM7:def 1;
h is_reducible_wrt q,T by A63, A65, A66, POLYRED:36;
then consider r being Polynomial of n,L such that
A69: h reduces_to r,q,T by POLYRED:def 8;
HT (q,T) <= HT (f,T),T by A65, A66, TERMORD:10;
then q <> h by A50, A53, A52, TERMORD:7;
then not q in {h} by TARSKI:def 1;
then q in H \ {h} by A67, XBOOLE_0:def 5;
then h reduces_to r,H \ {h},T by A69, POLYRED:def 7;
then h is_reducible_wrt H \ {h},T by POLYRED:def 9;
hence contradiction by A4, A39; :: thesis:

end;

hence contradiction ; :: thesis:

end;

suppose A70: g in H \ G ; :: thesis:

then A71: not g in G by XBOOLE_0:def 5;
A72: g in H by A70, XBOOLE_0:def 5;
then A73: g <> 0_ (n,L) by A17;
then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 1;
A74: H c= H -Ideal by IDEAL_1:def 14;
then HT (g,T) in HT ((G -Ideal),T) by A16, A5, A72, A73;
then consider b9 being bag of n such that
A75: b9 in HT (G,T) and
A76: b9 divides HT (g,T) by A23, Th18;
consider h being Polynomial of n,L such that
A77: b9 = HT (h,T) and
A78: h in G and
A79: h <> 0_ (n,L) by A75;
reconsider h = h as non-zero Polynomial of n,L by A79, POLYNOM7:def 1;
set f = g - h;

A80: now :: thesis:

assume A81: g - h = 0_ (n,L) ; :: thesis:
h = (0_ (n,L)) + h by POLYRED:2
.= (g + (- h)) + h by A81, POLYNOM1:def 7
.= g + ((- h) + h) by POLYNOM1:21
.= g + (0_ (n,L)) by POLYRED:3 ;
hence contradiction by A71, A78, POLYNOM1:23; :: thesis:

end;

Support g <> {} by A73, POLYNOM7:1;
then HT (g,T) in Support g by TERMORD:def 6;
then A82: g is_reducible_wrt h,T by A76, A77, POLYRED:36;
then A83: ex r being Polynomial of n,L st g reduces_to r,h,T by POLYRED:def 8;

now :: thesis:

assume not h in G \ H ; :: thesis:
then A84: h in H by A78, XBOOLE_0:def 5;
not h in {g} by A71, A78, TARSKI:def 1;
then h in H \ {g} by A84, XBOOLE_0:def 5;
then consider r being Polynomial of n,L such that
A85: ( h in H \ {g} & g reduces_to r,h,T ) by A83;
A86: g reduces_to r,H \ {g},T by A85, POLYRED:def 7;
g is_irreducible_wrt H \ {g},T by A4, A72;
hence contradiction by A86, POLYRED:def 9; :: thesis:

end;

then h in GH by A30, XBOOLE_0:def 3;
then g <= h,T by A15;
then not h < g,T by POLYRED:29;
then not HT (h,T) < HT (g,T),T by POLYRED:32;
then A87: HT (g,T) <= HT (h,T),T by TERMORD:5;
HT (h,T) <= HT (g,T),T by A82, Th9;
then A88: HT (h,T) = HT (g,T) by A87, TERMORD:7;
reconsider f = g - h as non-zero Polynomial of n,L by A80, POLYNOM7:def 1;
Support f <> {} by A80, POLYNOM7:1;
then A89: HT (f,T) in Support f by TERMORD:def 6;
f . (HT (g,T)) = (g + (- h)) . (HT (g,T)) by POLYNOM1:def 7
.= (g . (HT (g,T))) + ((- h) . (HT (g,T))) by POLYNOM1:15
.= (g . (HT (g,T))) + (- (h . (HT (h,T)))) by A88, POLYNOM1:17
.= (HC (g,T)) + (- (h . (HT (h,T)))) by TERMORD:def 7
.= (HC (g,T)) + (- (HC (h,T))) by TERMORD:def 7
.= (1. L) + (- (HC (h,T))) by A24, A72
.= (1. L) + (- (1. L)) by A24, A78
.= 0. L by RLVECT_1:5 ;
then A90: HT (f,T) <> HT (g,T) by A89, POLYNOM1:def 4;
HT (f,T) <= max ((HT (g,T)),(HT (h,T)),T),T by Th7;
then A91: HT (f,T) <= HT (g,T),T by A88, TERMORD:12;
reconsider g9 = g, h9 = h as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring (n,L)) ;
G c= G -Ideal by IDEAL_1:def 14;
then g9 - h9 in I by A16, A5, A72, A74, A78, IDEAL_1:15;
then f in I by Lm2;
then A92: HT (f,T) in HT (I,T) by A80;
Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:20;
then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 7;
then A93: Support f c= (Support g) \/ (Support h) by Th5;

now :: thesis:

per cases by A89, A93, XBOOLE_0:def 3;

case A94: HT (f,T) in Support g ; :: thesis:

consider b9 being bag of n such that
A95: b9 in HT (H,T) and
A96: b9 divides HT (f,T) by A5, A31, A92, Th18;
consider q being Polynomial of n,L such that
A97: b9 = HT (q,T) and
A98: q in H and
A99: q <> 0_ (n,L) by A95;
reconsider q = q as non-zero Polynomial of n,L by A99, POLYNOM7:def 1;
g is_reducible_wrt q,T by A94, A96, A97, POLYRED:36;
then consider r being Polynomial of n,L such that
A100: g reduces_to r,q,T by POLYRED:def 8;
HT (q,T) <= HT (f,T),T by A96, A97, TERMORD:10;
then q <> g by A91, A90, TERMORD:7;
then not q in {g} by TARSKI:def 1;
then q in H \ {g} by A98, XBOOLE_0:def 5;
then g reduces_to r,H \ {g},T by A100, POLYRED:def 7;
then g is_reducible_wrt H \ {g},T by POLYRED:def 9;
hence contradiction by A4, A72; :: thesis:

end;

case A101: HT (f,T) in Support h ; :: thesis:

consider b9 being bag of n such that
A102: b9 in HT (G,T) and
A103: b9 divides HT (f,T) by A16, A23, A92, Th18;
consider q being Polynomial of n,L such that
A104: b9 = HT (q,T) and
A105: q in G and
A106: q <> 0_ (n,L) by A102;
reconsider q = q as non-zero Polynomial of n,L by A106, POLYNOM7:def 1;
h is_reducible_wrt q,T by A101, A103, A104, POLYRED:36;
then consider r being Polynomial of n,L such that
A107: h reduces_to r,q,T by POLYRED:def 8;
HT (q,T) <= HT (f,T),T by A103, A104, TERMORD:10;
then HT (q,T) <> HT (h,T) by A88, A91, A90, TERMORD:7;
then not q in {h} by TARSKI:def 1;
then q in G \ {h} by A105, XBOOLE_0:def 5;
then h reduces_to r,G \ {h},T by A107, POLYRED:def 7;
then h is_reducible_wrt G \ {h},T by POLYRED:def 9;
hence contradiction by A2, A78; :: thesis:

end;

hence contradiction ; :: thesis:

end;