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 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 by Def7;
consider b being bag of n such that
A3: f reduces_to g,p,b,T by A2, Def6;
set b9 = b + (HT m,T);
A4: b in Support f by A3, Def5;

A5: now

m <> 0_ n,L by POLYNOM7:def 2;
then Support m <> {} by POLYNOM7:1;
then A6: m . (term m) <> 0. L by POLYNOM7:def 6;
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 5;
hence contradiction by A4, POLYNOM1:def 9; :: 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 9;
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, Def5;
reconsider p = p as non-zero Polynomial of n,L by A9, POLYNOM7:def 2;
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, Def5;
then reconsider f = f as non-zero Polynomial of n,L by POLYNOM7:def 2;
( m *' f <> 0_ n,L & p <> 0_ n,L ) by POLYNOM7:def 2;
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, Def5;
then A13: m *' f reduces_to (m *' f) - ((((m *' f) . (b + (HT m,T))) / (HC p,T)) * ((s + (HT m,T)) *' p)),p,T by Def6;
A14: (m . (term m)) * ((f . b) / (HC p,T)) = (m . (term m)) * ((f . b) * ((HC p,T) " )) by VECTSP_1:def 23
.= ((m . (term m)) * (f . b)) * ((HC p,T) " ) by GROUP_1:def 4
.= ((m . (term m)) * (f . b)) / (HC p,T) by VECTSP_1:def 23 ;
(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),(HT m,T)) *' (s *' p)))
.= (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 23
.= (m *' f) + (m *' (- (((f . b) / (HC p,T)) * (s *' p)))) by Th6
.= m *' (f + (- (((f . b) / (HC p,T)) * (s *' p)))) by POLYNOM1:85
.= m *' (f - (((f . b) / (HC p,T)) * (s *' p))) by POLYNOM1:def 23 ;
hence m *' f reduces_to m *' g,P,T by A1, A11, A13, Def7; :: thesis: verum