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 P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to g,P,T holds
m *' f reduces_to m *' g,P,T
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 P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to g,P,T holds
m *' f reduces_to m *' g,P,T
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 P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to g,P,T holds
m *' f reduces_to m *' g,P,T
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for f, g being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to g,P,T holds
m *' f reduces_to m *' g,P,T
let f, g be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L st f reduces_to g,P,T holds
m *' f reduces_to m *' g,P,T
let m be non-zero Monomial of n,L; :: thesis: ( f reduces_to g,P,T implies m *' f reduces_to m *' g,P,T )
assume f reduces_to g,P,T ; :: thesis: m *' f reduces_to m *' g,P,T
then consider p being Polynomial of n,L such that
A1: p in P and
A2: f reduces_to g,p,T ;
consider b being bag of n such that
A3: f reduces_to g,p,b,T by A2;
set b9 = b + (HT (m,T));
A4: b in Support f by A3;

A5: now :: thesis: not (m *' f) . (b + (HT (m,T))) = 0. L

m <> 0_ (n,L) by POLYNOM7:def 1;
then Support m <> {} by POLYNOM7:1;
then A6: m . (term m) <> 0. L by POLYNOM7:def 5;
assume A7: (m *' f) . (b + (HT (m,T))) = 0. L ; :: thesis: contradiction
(m *' f) . (b + (HT (m,T))) = (m *' f) . ((term m) + b) by TERMORD:23
.= (m . (term m)) * (f . b) by Th7 ;
then f . b = 0. L by A7, A6, VECTSP_2:def 1;
hence contradiction by A4, POLYNOM1:def 4; :: thesis: verum

end;

b + (HT (m,T)) is Element of Bags n by PRE_POLY:def 12;
then A8: b + (HT (m,T)) in Support (m *' f) by A5, POLYNOM1:def 4;
A9: p <> 0_ (n,L) by A2, Lm18;
consider s being bag of n such that
A10: s + (HT (p,T)) = b and
A11: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A3;
reconsider p = p as non-zero Polynomial of n,L by A9, POLYNOM7:def 1;
A12: (s + (HT (m,T))) + (HT (p,T)) = b + (HT (m,T)) by A10, PRE_POLY:35;
set t = s + (HT (m,T));
set h = (m *' f) - ((((m *' f) . (b + (HT (m,T)))) / (HC (p,T))) * ((s + (HT (m,T))) *' p));
f <> 0_ (n,L) by A3;
then reconsider f = f as non-zero Polynomial of n,L by POLYNOM7:def 1;
( m *' f <> 0_ (n,L) & p <> 0_ (n,L) ) by POLYNOM7:def 1;
then m *' f reduces_to (m *' f) - ((((m *' f) . (b + (HT (m,T)))) / (HC (p,T))) * ((s + (HT (m,T))) *' p)),p,b + (HT (m,T)),T by A8, A12;
then A13: m *' f reduces_to (m *' f) - ((((m *' f) . (b + (HT (m,T)))) / (HC (p,T))) * ((s + (HT (m,T))) *' p)),p,T ;
A14: (m . (term m)) * ((f . b) / (HC (p,T))) = (m . (term m)) * ((f . b) * ((HC (p,T)) "))
.= ((m . (term m)) * (f . b)) * ((HC (p,T)) ") by GROUP_1:def 3
.= ((m . (term m)) * (f . b)) / (HC (p,T)) ;
(m *' f) . (b + (HT (m,T))) = (m *' f) . ((term m) + b) by TERMORD:23
.= (m . (term m)) * (f . b) by Th7 ;
then (m *' f) - ((((m *' f) . (b + (HT (m,T)))) / (HC (p,T))) * ((s + (HT (m,T))) *' p)) = (m *' f) - (((m . (term m)) * ((f . b) / (HC (p,T)))) * ((HT (m,T)) *' (s *' p))) by A14, Th18
.= (m *' f) - (((f . b) / (HC (p,T))) * ((m . (term m)) * ((HT (m,T)) *' (s *' p)))) by Th11
.= (m *' f) - (((f . b) / (HC (p,T))) * ((Monom ((m . (term m)),(HT (m,T)))) *' (s *' p))) by Th22
.= (m *' f) - (((f . b) / (HC (p,T))) * ((Monom ((coefficient m),(term m))) *' (s *' p))) by TERMORD:23
.= (m *' f) - (((f . b) / (HC (p,T))) * (m *' (s *' p))) by POLYNOM7:11
.= (m *' f) - (m *' (((f . b) / (HC (p,T))) * (s *' p))) by Th12
.= (m *' f) + (- (m *' (((f . b) / (HC (p,T))) * (s *' p)))) by POLYNOM1:def 7
.= (m *' f) + (m *' (- (((f . b) / (HC (p,T))) * (s *' p)))) by Th6
.= m *' (f + (- (((f . b) / (HC (p,T))) * (s *' p)))) by POLYNOM1:26
.= m *' (f - (((f . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:def 7 ;
hence m *' f reduces_to m *' g,P,T by A1, A11, A13; :: thesis: verum