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 A1: ( G is_Groebner_basis_of I,T & G is_reduced_wrt T & H is_Groebner_basis_of I,T & H is_reduced_wrt T ) ; :: thesis:
assume A2: G <> H ; :: thesis:
A3: ( PolyRedRel G,T is locally-confluent & PolyRedRel H,T is locally-confluent ) by A1, Def4;
A4: ( G -Ideal = I & H -Ideal = I ) by A1, Def4;

A5: now

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

now

per cases by A6;

case A7: u in G ; :: thesis:

then reconsider u' = u as Element of (Polynom-Ring n,L) ;
reconsider u' = u' as Polynomial of n,L by POLYNOM1:def 27;
u' is_monic_wrt T by A1, A7, Def7;
then A8: HC u',T = 1. L by Def6;
1. L <> 0. L ;
hence ( u is Polynomial of n,L & u <> 0_ n,L ) by A8, TERMORD:17; :: thesis:

end;

case A9: u in H ; :: thesis:

then reconsider u' = u as Element of (Polynom-Ring n,L) ;
reconsider u' = u' as Polynomial of n,L by POLYNOM1:def 27;
u' is_monic_wrt T by A1, A9, Def7;
then A10: HC u',T = 1. L by Def6;
1. L <> 0. L ;
hence ( u is Polynomial of n,L & u <> 0_ n,L ) by A10, TERMORD:17; :: thesis:

end;

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

end;

A11: 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 A1, Def7;
hence HC u,T = 1. L by Def6; :: thesis:

end;

set GH = (G \/ H) \ (G /\ H);

now

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

A13: 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 A12, XBOOLE_0:def 4; :: thesis:

end;

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 A12, XBOOLE_0:def 4; :: thesis:

end;

hence contradiction by A2, A13, TARSKI:2; :: thesis:

end;

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

A14: now

let u be set ; :: thesis:
assume u in GH ; :: thesis:
then A15: ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 5;
( u in G \ H or u in H \ G )

proof

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

now

per cases by A16, XBOOLE_0:def 5;

case not u in G ; :: thesis:

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

end;

case u in H ; :: thesis:

hence ( u in H & not u in G ) by A15, 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;

now

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

now

per cases by A17, 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 A18: GH = (G \ H) \/ (H \ G) by A14, TARSKI:2;

A19: now

let u be set ; :: thesis:
assume u in GH ; :: thesis:
then A20: ( u in G \/ H & not u in G /\ H ) by XBOOLE_0:def 5;
then A21: ( not u in G or not u in H ) by XBOOLE_0:def 4;

now

per cases by A20, XBOOLE_0:def 3;

case u in G ; :: thesis:

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

end;

case u in H ; :: thesis:

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

end;

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

end;

consider g being Polynomial of n,L such that
A22: ( g in GH & ( for q being Polynomial of n,L st q in GH holds
g <= q,T ) ) by POLYRED:31;
PolyRedRel H,T is with_UN_property 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 A23: for f being non-zero Polynomial of n,L st f in H -Ideal holds
f is_top_reducible_wrt H,T by Th17;
PolyRedRel G,T is with_UN_property by A3;
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 A24: for f being non-zero Polynomial of n,L st f in G -Ideal holds
f is_top_reducible_wrt G,T by Th17;

per cases by A19, A22;

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

then A26: ( g in G & not g in H ) by XBOOLE_0:def 5;
A27: G c= G -Ideal by IDEAL_1:def 15;
then A28: ( g in H -Ideal & g <> 0_ n,L ) by A4, A5, A26;
then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 2;
HT g,T in HT (H -Ideal ),T by A28;
then consider b' being bag of such that
A29: ( b' in HT H,T & b' divides HT g,T ) by A23, Th18;
consider h being Polynomial of n,L such that
A30: ( b' = HT h,T & h in H & h <> 0_ n,L ) by A29;
reconsider h = h as non-zero Polynomial of n,L by A30, POLYNOM7:def 2;
A31: H c= H -Ideal by IDEAL_1:def 15;
A32: h <> g by A25, A30, XBOOLE_0:def 5;
Support g <> {} by A28, POLYNOM7:1;
then HT g,T in Support g by TERMORD:def 6;
then A33: g is_reducible_wrt h,T by A29, A30, POLYRED:36;
then A34: 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 A35: h in G by A30, XBOOLE_0:def 5;
A36: g is_irreducible_wrt G \ {g},T by A1, A26, Def7;
not h in {g} by A32, TARSKI:def 1;
then h in G \ {g} by A35, XBOOLE_0:def 5;
then consider r being Polynomial of n,L such that
A37: ( h in G \ {g} & g reduces_to r,h,T ) by A34;
g reduces_to r,G \ {g},T by A37, POLYRED:def 7;
hence contradiction by A36, POLYRED:def 9; :: thesis:

end;

then h in GH by A18, XBOOLE_0:def 3;
then g <= h,T by A22;
then not h < g,T by POLYRED:29;
then not HT h,T < HT g,T,T by POLYRED:32;
then A38: HT g,T <= HT h,T,T by TERMORD:5;
HT h,T <= HT g,T,T by A33, Th9;
then A39: HT h,T = HT g,T by A38, TERMORD:7;
set f = g - h;

A40: now

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

end;

then reconsider f = g - h as non-zero Polynomial of n,L by POLYNOM7:def 2;
Support f <> {} by A40, POLYNOM7:1;
then A42: HT f,T in Support f by TERMORD:def 6;
HT f,T <= max (HT g,T),(HT h,T),T,T by Th7;
then A43: HT f,T <= HT g,T,T by A39, TERMORD:12;
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 A39, 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 A11, A26
.= (1. L) + (- (1. L)) by A11, A30
.= 0. L by RLVECT_1:16 ;
then A44: HT f,T <> HT g,T by A42, POLYNOM1:def 9;
Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:79;
then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 23;
then A45: Support f c= (Support g) \/ (Support h) by Th5;
reconsider g' = g, h' = h as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider g' = g', h' = h' as Element of (Polynom-Ring n,L) ;
g' - h' in I by A4, A26, A27, A30, A31, IDEAL_1:15;
then f in I by Lm2;
then A46: HT f,T in HT I,T by A40;

now

per cases by A42, A45, XBOOLE_0:def 3;

case A47: HT f,T in Support g ; :: thesis:

consider b' being bag of such that
A48: ( b' in HT G,T & b' divides HT f,T ) by A4, A24, A46, Th18;
consider q being Polynomial of n,L such that
A49: ( b' = HT q,T & q in G & q <> 0_ n,L ) by A48;
reconsider q = q as non-zero Polynomial of n,L by A49, POLYNOM7:def 2;
g is_reducible_wrt q,T by A47, A48, A49, POLYRED:36;
then consider r being Polynomial of n,L such that
A50: g reduces_to r,q,T by POLYRED:def 8;
HT q,T <= HT f,T,T by A48, A49, TERMORD:10;
then q <> g by A43, A44, TERMORD:7;
then not q in {g} by TARSKI:def 1;
then q in G \ {g} by A49, XBOOLE_0:def 5;
then g reduces_to r,G \ {g},T by A50, POLYRED:def 7;
then g is_reducible_wrt G \ {g},T by POLYRED:def 9;
hence contradiction by A1, A26, Def7; :: thesis:

end;

case A51: HT f,T in Support h ; :: thesis:

consider b' being bag of such that
A52: ( b' in HT H,T & b' divides HT f,T ) by A4, A23, A46, Th18;
consider q being Polynomial of n,L such that
A53: ( b' = HT q,T & q in H & q <> 0_ n,L ) by A52;
reconsider q = q as non-zero Polynomial of n,L by A53, POLYNOM7:def 2;
h is_reducible_wrt q,T by A51, A52, A53, POLYRED:36;
then consider r being Polynomial of n,L such that
A54: h reduces_to r,q,T by POLYRED:def 8;
HT q,T <= HT f,T,T by A52, A53, TERMORD:10;
then q <> h by A39, A43, A44, TERMORD:7;
then not q in {h} by TARSKI:def 1;
then q in H \ {h} by A53, XBOOLE_0:def 5;
then h reduces_to r,H \ {h},T by A54, POLYRED:def 7;
then h is_reducible_wrt H \ {h},T by POLYRED:def 9;
hence contradiction by A1, A30, Def7; :: thesis:

end;

hence contradiction ; :: thesis:

end;

suppose g in H \ G ; :: thesis:

then A55: ( g in H & not g in G ) by XBOOLE_0:def 5;
A56: H c= H -Ideal by IDEAL_1:def 15;
then A57: ( g in G -Ideal & g <> 0_ n,L ) by A4, A5, A55;
then reconsider g = g as non-zero Polynomial of n,L by POLYNOM7:def 2;
HT g,T in HT (G -Ideal ),T by A57;
then consider b' being bag of such that
A58: ( b' in HT G,T & b' divides HT g,T ) by A24, Th18;
consider h being Polynomial of n,L such that
A59: ( b' = HT h,T & h in G & h <> 0_ n,L ) by A58;
reconsider h = h as non-zero Polynomial of n,L by A59, POLYNOM7:def 2;
A60: G c= G -Ideal by IDEAL_1:def 15;
Support g <> {} by A57, POLYNOM7:1;
then HT g,T in Support g by TERMORD:def 6;
then A61: g is_reducible_wrt h,T by A58, A59, POLYRED:36;
then A62: 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 A63: h in H by A59, XBOOLE_0:def 5;
A64: g is_irreducible_wrt H \ {g},T by A1, A55, Def7;
not h in {g} by A55, A59, TARSKI:def 1;
then h in H \ {g} by A63, XBOOLE_0:def 5;
then consider r being Polynomial of n,L such that
A65: ( h in H \ {g} & g reduces_to r,h,T ) by A62;
g reduces_to r,H \ {g},T by A65, POLYRED:def 7;
hence contradiction by A64, POLYRED:def 9; :: thesis:

end;

then h in GH by A18, XBOOLE_0:def 3;
then g <= h,T by A22;
then not h < g,T by POLYRED:29;
then not HT h,T < HT g,T,T by POLYRED:32;
then A66: HT g,T <= HT h,T,T by TERMORD:5;
HT h,T <= HT g,T,T by A61, Th9;
then A67: HT h,T = HT g,T by A66, TERMORD:7;
set f = g - h;

A68: now

assume A69: g - h = 0_ n,L ; :: thesis:
h = (0_ n,L) + h by POLYRED:2
.= (g + (- h)) + h by A69, POLYNOM1:def 23
.= g + ((- h) + h) by POLYNOM1:80
.= g + (0_ n,L) by POLYRED:3 ;
hence contradiction by A55, A59, POLYNOM1:82; :: thesis:

end;

then reconsider f = g - h as non-zero Polynomial of n,L by POLYNOM7:def 2;
Support f <> {} by A68, POLYNOM7:1;
then A70: HT f,T in Support f by TERMORD:def 6;
HT f,T <= max (HT g,T),(HT h,T),T,T by Th7;
then A71: HT f,T <= HT g,T,T by A67, TERMORD:12;
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 A67, 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 A11, A55
.= (1. L) + (- (1. L)) by A11, A59
.= 0. L by RLVECT_1:16 ;
then A72: HT f,T <> HT g,T by A70, POLYNOM1:def 9;
Support (g + (- h)) c= (Support g) \/ (Support (- h)) by POLYNOM1:79;
then Support f c= (Support g) \/ (Support (- h)) by POLYNOM1:def 23;
then A73: Support f c= (Support g) \/ (Support h) by Th5;
reconsider g' = g, h' = h as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider g' = g', h' = h' as Element of (Polynom-Ring n,L) ;
g' - h' in I by A4, A55, A56, A59, A60, IDEAL_1:15;
then f in I by Lm2;
then A74: HT f,T in HT I,T by A68;

now

per cases by A70, A73, XBOOLE_0:def 3;

case A75: HT f,T in Support g ; :: thesis:

consider b' being bag of such that
A76: ( b' in HT H,T & b' divides HT f,T ) by A4, A23, A74, Th18;
consider q being Polynomial of n,L such that
A77: ( b' = HT q,T & q in H & q <> 0_ n,L ) by A76;
reconsider q = q as non-zero Polynomial of n,L by A77, POLYNOM7:def 2;
g is_reducible_wrt q,T by A75, A76, A77, POLYRED:36;
then consider r being Polynomial of n,L such that
A78: g reduces_to r,q,T by POLYRED:def 8;
HT q,T <= HT f,T,T by A76, A77, TERMORD:10;
then q <> g by A71, A72, TERMORD:7;
then not q in {g} by TARSKI:def 1;
then q in H \ {g} by A77, XBOOLE_0:def 5;
then g reduces_to r,H \ {g},T by A78, POLYRED:def 7;
then g is_reducible_wrt H \ {g},T by POLYRED:def 9;
hence contradiction by A1, A55, Def7; :: thesis:

end;

case A79: HT f,T in Support h ; :: thesis:

consider b' being bag of such that
A80: ( b' in HT G,T & b' divides HT f,T ) by A4, A24, A74, Th18;
consider q being Polynomial of n,L such that
A81: ( b' = HT q,T & q in G & q <> 0_ n,L ) by A80;
reconsider q = q as non-zero Polynomial of n,L by A81, POLYNOM7:def 2;
h is_reducible_wrt q,T by A79, A80, A81, POLYRED:36;
then consider r being Polynomial of n,L such that
A82: h reduces_to r,q,T by POLYRED:def 8;
HT q,T <= HT f,T,T by A80, A81, TERMORD:10;
then HT q,T <> HT h,T by A67, A71, A72, TERMORD:7;
then not q in {h} by TARSKI:def 1;
then q in G \ {h} by A81, XBOOLE_0:def 5;
then h reduces_to r,G \ {h},T by A82, POLYRED:def 7;
then h is_reducible_wrt G \ {h},T by POLYRED:def 9;
hence contradiction by A1, A59, Def7; :: thesis:

end;

hence contradiction ; :: thesis:

end;