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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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, Def4;
set GH = (G \/ H) \ (G /\ H);
assume A6: G <> H ; :: thesis:

now

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

A8: now

let u be set ; :: 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

let u be set ; :: 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

let u be set ; :: 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

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

A17: now

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

now

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 27;
u9 is_monic_wrt T by A2, A19, Def7;
then A20: HC u9,T = 1. L by Def6;
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 27;
u9 is_monic_wrt T by A4, A21, Def7;
then A22: HC u9,T = 1. L by Def6;
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, Def4;
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: now

let u be Polynomial of n,L; :: thesis:
assume ( u in G or u in H ) ; :: thesis:
then u is_monic_wrt T by A2, A4, Def7;
hence HC u,T = 1. L by Def6; :: thesis:

end;

A25: now

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

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

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

now

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, Def4;
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 2;
A35: G c= G -Ideal by IDEAL_1:def 15;
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 2;
set f = g - h;
A41: h <> g by A32, A39, XBOOLE_0:def 5;

A42: now

assume A43: g - h = 0_ n,L ; :: thesis:
h = (0_ n,L) + h by POLYRED:2
.= (g + (- h)) + h by A43, POLYNOM1:def 23
.= g + ((- h) + h) by POLYNOM1:80
.= g + (0_ n,L) by POLYRED:3 ;
hence contradiction by A41, POLYNOM1:82; :: 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

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, Def7;
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 2;
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 23
.= (g . (HT g,T)) + ((- h) . (HT g,T)) by POLYNOM1:def 21
.= (g . (HT g,T)) + (- (h . (HT h,T))) by A50, POLYNOM1:def 22
.= (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:16 ;
then A52: HT f,T <> HT g,T by A51, POLYNOM1:def 9;
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 27;
reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring n,L) ;
H c= H -Ideal by IDEAL_1:def 15;
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:79;
then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 23;
then A55: Support f c= (Support g) \/ (Support h) by Th5;

now

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 2;
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, Def7; :: 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 2;
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, Def7; :: 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 2;
A74: H c= H -Ideal by IDEAL_1:def 15;
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 2;
set f = g - h;

A80: now

assume A81: g - h = 0_ n,L ; :: thesis:
h = (0_ n,L) + h by POLYRED:2
.= (g + (- h)) + h by A81, POLYNOM1:def 23
.= g + ((- h) + h) by POLYNOM1:80
.= g + (0_ n,L) by POLYRED:3 ;
hence contradiction by A71, A78, POLYNOM1:82; :: 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

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, Def7;
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 2;
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 23
.= (g . (HT g,T)) + ((- h) . (HT g,T)) by POLYNOM1:def 21
.= (g . (HT g,T)) + (- (h . (HT h,T))) by A88, POLYNOM1:def 22
.= (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:16 ;
then A90: HT f,T <> HT g,T by A89, POLYNOM1:def 9;
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 27;
reconsider g9 = g9, h9 = h9 as Element of (Polynom-Ring n,L) ;
G c= G -Ideal by IDEAL_1:def 15;
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:79;
then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 23;
then A93: Support f c= (Support g) \/ (Support h) by Th5;

now

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 2;
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, Def7; :: 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 2;
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, Def7; :: thesis:

end;

hence contradiction ; :: thesis:

end;