let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) holds
f + g reduces_to f1 + g,{p},T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) holds
f + g reduces_to f1 + g,{p},T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f, f1, g, p being Polynomial of n,L st f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) holds
f + g reduces_to f1 + g,{p},T
let f, f1, g, p be Polynomial of n,L; :: thesis: ( f reduces_to f1,{p},T & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) implies f + g reduces_to f1 + g,{p},T )
assume that
A1: f reduces_to f1,{p},T and
A2: for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ; :: thesis: f + g reduces_to f1 + g,{p},T
consider q being Polynomial of n,L such that
A3: q in {p} and
A4: f reduces_to f1,q,T by A1, POLYRED:def 7;
p = q by A3, TARSKI:def 1;
then consider br being bag of n such that
A5: f reduces_to f1,p,br,T by A4, POLYRED:def 6;
consider s being bag of n such that
A6: s + (HT (p,T)) = br and
A7: f1 = f - (((f . br) / (HC (p,T))) * (s *' p)) by A5, POLYRED:def 5;

A8: now

assume A9: br in Support g ; :: thesis: contradiction
HT (p,T) divides br by A6, TERMORD:1;
hence contradiction by A2, A9; :: thesis: verum

end;

A10: br is Element of Bags n by PRE_POLY:def 12;
A11: p in {p} by TARSKI:def 1;
A12: br in Support f by A5, POLYRED:def 5;
A13: (f + g) . br = (f . br) + (g . br) by POLYNOM1:15
.= (f . br) + (0. L) by A8, A10, POLYNOM1:def 3
.= f . br by RLVECT_1:def 4 ;
A14: p <> 0_ (n,L) by A5, POLYRED:def 5;

now

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

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

then (f + g) - f = - f by Th14;
then (f + g) + (- f) = - f by POLYNOM1:def 6;
then (f + (- f)) + g = - f by POLYNOM1:21;
then (0_ (n,L)) + g = - f by POLYRED:3;
then g = - f by POLYRED:2;
hence contradiction by A12, A8, GROEB_1:5; :: thesis: verum

end;

case A15: f + g <> 0_ (n,L) ; :: thesis: f + g reduces_to f1 + g,{p},T

set g1 = (f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p));
(f + g) . br <> 0. L by A12, A13, POLYNOM1:def 3;
then br in Support (f + g) by A12, POLYNOM1:def 3;
then f + g reduces_to (f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p)),p,br,T by A14, A6, A15, POLYRED:def 5;
then A16: f + g reduces_to (f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p)),p,T by POLYRED:def 6;
(f + g) - ((((f + g) . br) / (HC (p,T))) * (s *' p)) = (f + g) + (- (((f . br) / (HC (p,T))) * (s *' p))) by A13, POLYNOM1:def 6
.= (f + (- (((f . br) / (HC (p,T))) * (s *' p)))) + g by POLYNOM1:21
.= f1 + g by A7, POLYNOM1:def 6 ;
hence f + g reduces_to f1 + g,{p},T by A11, A16, POLYRED:def 7; :: thesis: verum

end;

end;

end;

hence f + g reduces_to f1 + g,{p},T ; :: thesis: verum