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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 that
A1: f in I and
A2: g in I and
A3: HM (f,T) = m and
A4: 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 )
A5: HT (f,T) = term (HM (f,T)) by TERMORD:22
.= HT (g,T) by A3, A4, TERMORD:22 ;
A6: 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 A3, A4, A5, TERMORD:18
.= HC (g,T) by TERMORD:def 7 ;
assume that
A7: for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) and
A8: 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
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 7
.= f + ((- g) + g) by POLYNOM1:21
.= f + (0_ (n,L)) by POLYRED:3
.= f by POLYNOM1:23 ;
:: thesis: verum

end;

suppose A9: f - g <> 0_ (n,L) ; :: thesis: f = g

now :: thesis: ( ( f = 0_ (n,L) & f = g ) or ( g = 0_ (n,L) & f = g ) or ( f <> 0_ (n,L) & g <> 0_ (n,L) & contradiction ) )

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

case A10: f = 0_ (n,L) ; :: thesis: f = g

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

end;

case A11: g = 0_ (n,L) ; :: thesis: f = g

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

end;

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

set s = HT ((f - g),T);
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));
A13: Support (f - g) <> {} by A9, POLYNOM7:1;
then A14: HT ((f - g),T) in Support (f - g) by TERMORD:def 6;

A15: now :: thesis: not HT ((f - g),T) = HT (f,T)

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 7
.= (f . (HT (f,T))) + ((- g) . (HT (g,T))) by A5, POLYNOM1:15
.= (f . (HT (f,T))) + (- (g . (HT (g,T)))) by POLYNOM1:17
.= (HC (f,T)) + (- (g . (HT (g,T)))) by TERMORD:def 7
.= (HC (f,T)) + (- (HC (g,T))) by TERMORD:def 7
.= 0. L by A6, RLVECT_1:5 ;
hence contradiction by A14, POLYNOM1:def 4; :: thesis: verum

end;

HT ((f - g),T) <= max ((HT (f,T)),(HT (f,T)),T),T by A5, Th7;
then HT ((f - g),T) <= HT (f,T),T by TERMORD:12;
then HT ((f - g),T) < HT (f,T),T by A15, 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 A16: (f - g) . (HT (f,T)) = 0. L by POLYNOM1:def 4;
A17: (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 7
.= (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:15
.= (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:17
.= (f . (HT (f,T))) + (- (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (0. L))) by A16, POLYNOM7:def 9
.= (f . (HT (f,T))) + (- (0. L))
.= (f . (HT (f,T))) + (0. L) by RLVECT_1:12
.= f . (HT (f,T)) by RLVECT_1:def 4 ;
Support f <> {} by A12, POLYNOM7:1;
then HT (f,T) in Support f by TERMORD:def 6;
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 A17, POLYNOM1:def 4;
then A18: 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 4;
then A19: 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;
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 7;
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:20;
then A20: 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 A21: 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 A20;
not g < f,T by A2, A4, A7;
then A22: f <= g,T by POLYRED:29;
not f < g,T by A1, A3, A8;
then g <= f,T by POLYRED:29;
then A23: Support f = Support g by A22, POLYRED:26;
( Support (f - g) = Support (f + (- g)) & Support (f + (- g)) c= (Support f) \/ (Support (- g)) ) by POLYNOM1:20, POLYNOM1:def 7;
then A24: Support (f - g) c= (Support f) \/ (Support g) by Th5;
then A25: (Support f) \/ (Support (f - g)) c= (Support f) \/ (Support f) by A23, XBOOLE_1:9;
then A26: Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) c= Support f by A21;
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 A18, 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 A26, TERMORD:def 6;
then A27: HT ((f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))),T) = HT (f,T) by A19, 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 A17, TERMORD:def 7
.= HC (f,T) by TERMORD:def 7 ;
then A28: 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 A27, TERMORD:def 8
.= m by A3, TERMORD:def 8 ;
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 11;
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 11;
reconsider f9 = f, g9 = g as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A29: (f - g) . (HT ((f - g),T)) = (f + (- g)) . (HT ((f - g),T)) by POLYNOM1:def 7
.= (f . (HT ((f - g),T))) + ((- g) . (HT ((f - g),T))) by POLYNOM1:15
.= (f . (HT ((f - g),T))) + (- (g . (HT ((f - g),T)))) by POLYNOM1:17
.= (f . (HT ((f - g),T))) - (g . (HT ((f - g),T))) ;
A30: HT ((f - g),T) in Support (f - g) by A13, TERMORD:def 6;

A31: now :: thesis: not Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) = Support f

A32: (f - g) . (HT ((f - g),T)) <> 0. L by A30, POLYNOM1:def 4;
A33: - (((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 3
.= - ((f . (HT ((f - g),T))) * (1. L)) by A29, A32, VECTSP_1:def 10
.= - (f . (HT ((f - g),T))) ;
assume A34: Support (f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g))) = Support f ; :: thesis: contradiction
(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 7
.= (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:15
.= (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 9
.= (f . (HT ((f - g),T))) + (- (f . (HT ((f - g),T)))) by A29, A33, VECTSP_1:9
.= 0. L by RLVECT_1:5 ;
hence contradiction by A23, A14, A24, A34, POLYNOM1:def 4; :: thesis: verum

end;

f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)) <= f,T by A21, A25, Th8, XBOOLE_1:1;
then A35: f - (((f . (HT ((f - g),T))) * (((f . (HT ((f - g),T))) - (g . (HT ((f - g),T)))) ")) * (f - g)) < f,T by A31, POLYRED:def 3;
reconsider cp = cp as Element of (Polynom-Ring (n,L)) ;
reconsider cc = cc as Element of (Polynom-Ring (n,L)) ;
reconsider f9 = f9, g9 = g9 as Element of (Polynom-Ring (n,L)) ;
f - g = f9 - g9 by Lm2;
then A36: cp = cc * (f9 - g9) by POLYNOM1:def 11;
f9 - g9 in I by A1, A2, IDEAL_1:15;
then A37: cc * (f9 - g9) in I by IDEAL_1:def 2;
f9 - 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 A1, A7, A28, A35, A37, A36, IDEAL_1:15; :: thesis: verum

end;

end;

end;

hence f = g ; :: thesis: verum

end;

end;