let n be Ordinal; :: 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 I being add-closed left-ideal Subset of (Polynom-Ring n,L)
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM f,T = m & HM g,T = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) holds
f = g
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 I being add-closed left-ideal Subset of (Polynom-Ring n,L)
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM f,T = m & HM g,T = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) holds
f = g
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 I being add-closed left-ideal Subset of (Polynom-Ring n,L)
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM f,T = m & HM g,T = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) holds
f = g
let I be add-closed left-ideal Subset of (Polynom-Ring n,L); :: thesis: for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM f,T = m & HM g,T = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) holds
f = g
let m be Monomial of n,L; :: thesis: for f, g being Polynomial of n,L st f in I & g in I & HM f,T = m & HM g,T = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) holds
f = g
let f, g be Polynomial of n,L; :: thesis: ( f in I & g in I & HM f,T = m & HM g,T = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) implies f = g )
assume A1: ( f in I & g in I & HM f,T = m & HM g,T = m ) ; :: thesis: ( ex p being Polynomial of n,L st
( p in I & p < f,T & HM p,T = m ) or ex p being Polynomial of n,L st
( p in I & p < g,T & HM p,T = m ) or f = g )
assume A2: ( ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM p,T = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM p,T = m ) ) ) ; :: thesis: f = g
A3: HT f,T = term (HM f,T) by TERMORD:22
.= HT g,T by A1, TERMORD:22 ;
A4: HC f,T = f . (HT f,T) by TERMORD:def 7
.= (HM f,T) . (HT f,T) by TERMORD:18
.= g . (HT g,T) by A1, A3, TERMORD:18
.= HC g,T by TERMORD:def 7 ;
reconsider I = I as LeftIdeal of (Polynom-Ring n,L) by A1;

per cases ( f - g = 0_ n,L or f - g <> 0_ n,L ) ;

suppose f - g = 0_ n,L ; :: thesis: f = g

hence g = (f - g) + g by POLYRED:2
.= (f + (- g)) + g by POLYNOM1:def 23
.= f + ((- g) + g) by POLYNOM1:80
.= f + (0_ n,L) by POLYRED:3
.= f by POLYNOM1:82 ;
:: thesis: verum

end;

suppose A5: f - g <> 0_ n,L ; :: thesis: f = g

now

per cases ( f = 0_ n,L or g = 0_ n,L or ( f <> 0_ n,L & g <> 0_ n,L ) ) ;

case A6: f = 0_ n,L ; :: thesis: f = g

then HC g,T = 0. L by A4, TERMORD:17;
hence f = g by A6, TERMORD:17; :: thesis: verum

end;

case A7: g = 0_ n,L ; :: thesis: f = g

then HC f,T = 0. L by A4, TERMORD:17;
hence f = g by A7, TERMORD:17; :: thesis: verum

end;

case ( f <> 0_ n,L & g <> 0_ n,L ) ; :: thesis: contradiction

then ( Support f <> {} & Support g <> {} ) by POLYNOM7:1;
then A8: ( HT f,T in Support f & ( for b being bag of st b in Support f holds
b <= HT f,T,T ) ) by TERMORD:def 6;
( not f < g,T & not g < f,T ) by A1, A2;
then ( f <= g,T & g <= f,T ) by POLYRED:29;
then A9: Support f = Support g by POLYRED:26;
HT (f - g),T <= max (HT f,T),(HT f,T),T,T by A3, Th7;
then A10: HT (f - g),T <= HT f,T,T by TERMORD:12;
A11: Support (f - g) <> {} by A5, POLYNOM7:1;
then A12: ( HT (f - g),T in Support (f - g) & ( for b being bag of st b in Support (f - g) holds
b <= HT (f - g),T,T ) ) by TERMORD:def 6;

now

assume HT (f - g),T = HT f,T ; :: thesis: contradiction
then (f - g) . (HT (f - g),T) = (f + (- g)) . (HT f,T) by POLYNOM1:def 23
.= (f . (HT f,T)) + ((- g) . (HT g,T)) by A3, POLYNOM1:def 21
.= (f . (HT f,T)) + (- (g . (HT g,T))) by POLYNOM1:def 22
.= (HC f,T) + (- (g . (HT g,T))) by TERMORD:def 7
.= (HC f,T) + (- (HC g,T)) by TERMORD:def 7
.= 0. L by A4, RLVECT_1:16 ;
hence contradiction by A12, POLYNOM1:def 9; :: thesis: verum

end;

then HT (f - g),T < HT f,T,T by A10, TERMORD:def 3;
then not HT f,T <= HT (f - g),T,T by TERMORD:5;
then not HT f,T in Support (f - g) by TERMORD:def 6;
then A13: (f - g) . (HT f,T) = 0. L by POLYNOM1:def 9;
set s = HT (f - g),T;
A14: Support (f - g) = Support (f + (- g)) by POLYNOM1:def 23;
Support (f + (- g)) c= (Support f) \/ (Support (- g)) by POLYNOM1:79;
then A15: Support (f - g) c= (Support f) \/ (Support g) by A14, Th5;
A16: HT (f - g),T in Support (f - g) by A11, TERMORD:def 6;
set d = (f . (HT (f - g),T)) - (g . (HT (f - g),T));
set c = (f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " );
set h = f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g));
A17: (f - g) . (HT (f - g),T) = (f + (- g)) . (HT (f - g),T) by POLYNOM1:def 23
.= (f . (HT (f - g),T)) + ((- g) . (HT (f - g),T)) by POLYNOM1:def 21
.= (f . (HT (f - g),T)) + (- (g . (HT (f - g),T))) by POLYNOM1:def 22
.= (f . (HT (f - g),T)) - (g . (HT (f - g),T)) by RLVECT_1:def 12 ;
Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) = Support (f + (- (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)))) by POLYNOM1:def 23;
then Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) c= (Support f) \/ (Support (- (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)))) by POLYNOM1:79;
then A18: Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) c= (Support f) \/ (Support (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) by Th5;
(Support f) \/ (Support (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) c= (Support f) \/ (Support (f - g)) by POLYRED:19, XBOOLE_1:9;
then A19: Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) c= (Support f) \/ (Support (f - g)) by A18, XBOOLE_1:1;
A20: (Support f) \/ (Support (f - g)) c= (Support f) \/ (Support f) by A9, A15, XBOOLE_1:9;
then A21: Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) c= Support f by A19, XBOOLE_1:1;
A22: (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) . (HT f,T) = (f + (- (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)))) . (HT f,T) by POLYNOM1:def 23
.= (f . (HT f,T)) + ((- (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) . (HT f,T)) by POLYNOM1:def 21
.= (f . (HT f,T)) + (- ((((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)) . (HT f,T))) by POLYNOM1:def 22
.= (f . (HT f,T)) + (- (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (0. L))) by A13, POLYNOM7:def 10
.= (f . (HT f,T)) + (- (0. L)) by VECTSP_1:39
.= (f . (HT f,T)) + (0. L) by RLVECT_1:25
.= f . (HT f,T) by RLVECT_1:def 7 ;
then (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) . (HT f,T) <> 0. L by A8, POLYNOM1:def 9;
then A23: HT f,T in Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) by POLYNOM1:def 9;
then A24: HT f,T <= HT (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))),T,T by TERMORD:def 6;
HT (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))),T in Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) by A23, TERMORD:def 6;
then HT (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))),T <= HT f,T,T by A21, TERMORD:def 6;
then A25: HT (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))),T = HT f,T by A24, TERMORD:7;
then HC (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))),T = f . (HT f,T) by A22, TERMORD:def 7
.= HC f,T by TERMORD:def 7 ;
then A26: HM (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))),T = Monom (HC f,T),(HT f,T) by A25, TERMORD:def 8
.= m by A1, TERMORD:def 8 ;
A27: f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)) <= f,T by A19, A20, Th8, XBOOLE_1:1;

now

assume A28: Support (f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) = Support f ; :: thesis: contradiction
A29: (f - g) . (HT (f - g),T) <> 0. L by A16, POLYNOM1:def 9;
A30: - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * ((f . (HT (f - g),T)) - (g . (HT (f - g),T)))) = - ((f . (HT (f - g),T)) * ((((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " ) * ((f . (HT (f - g),T)) - (g . (HT (f - g),T))))) by GROUP_1:def 4
.= - ((f . (HT (f - g),T)) * (1. L)) by A17, A29, VECTSP_1:def 22
.= - (f . (HT (f - g),T)) by VECTSP_1:def 19 ;
(f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) . (HT (f - g),T) = (f + (- (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)))) . (HT (f - g),T) by POLYNOM1:def 23
.= (f . (HT (f - g),T)) + ((- (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g))) . (HT (f - g),T)) by POLYNOM1:def 21
.= (f . (HT (f - g),T)) + (((- ((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " ))) * (f - g)) . (HT (f - g),T)) by POLYRED:9
.= (f . (HT (f - g),T)) + ((- ((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " ))) * ((f - g) . (HT (f - g),T))) by POLYNOM7:def 10
.= (f . (HT (f - g),T)) + (- (f . (HT (f - g),T))) by A17, A30, VECTSP_1:41
.= 0. L by RLVECT_1:16 ;
hence contradiction by A9, A12, A15, A28, POLYNOM1:def 9; :: thesis: verum

end;

then A31: f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)) < f,T by A27, POLYRED:def 3;
reconsider f' = f, g' = g as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider f' = f', g' = g' as Element of (Polynom-Ring n,L) ;
reconsider cc = ((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) | n,L as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider cc = cc as Element of (Polynom-Ring n,L) ;
f' - g' in I by A1, IDEAL_1:15;
then cc * (f' - g') in I by IDEAL_1:def 2;
then A32: f' - (cc * (f' - g')) in I by A1, IDEAL_1:15;
A33: f - g = f' - g' by Lm2;
reconsider cp = (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) | n,L) *' (f - g) as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider cp = cp as Element of (Polynom-Ring n,L) ;
A34: cp = cc * (f' - g') by A33, POLYNOM1:def 27;
f' - cp = f - ((((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) | n,L) *' (f - g)) by Lm2
.= f - (((f . (HT (f - g),T)) * (((f . (HT (f - g),T)) - (g . (HT (f - g),T))) " )) * (f - g)) by POLYNOM7:27 ;
hence contradiction by A2, A26, A31, A32, A34; :: thesis: verum

end;

end;

end;

hence f = g ; :: thesis: verum

end;

end;