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 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 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 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 st b1 in Support g holds
not HT p,T divides b1 ) implies f + g reduces_to f1 + g,{p},T )
assume A1: ( f reduces_to f1,{p},T & ( for b1 being bag of st b1 in Support g holds
not HT p,T divides b1 ) ) ; :: thesis: f + g reduces_to f1 + g,{p},T
then consider q being Polynomial of n,L such that
A2: ( q in {p} & f reduces_to f1,q,T ) by POLYRED:def 7;
A3: ( p = q & p in {p} ) by A2, TARSKI:def 1;
then consider br being bag of such that
A4: f reduces_to f1,p,br,T by A2, POLYRED:def 6;
A5: ( f <> 0_ n,L & p <> 0_ n,L & br in Support f & ex s being bag of st
( s + (HT p,T) = br & f1 = f - (((f . br) / (HC p,T)) * (s *' p)) ) ) by A4, POLYRED:def 5;
consider s being bag of such that
A6: ( s + (HT p,T) = br & f1 = f - (((f . br) / (HC p,T)) * (s *' p)) ) by A4, POLYRED:def 5;

A7: now

assume A8: br in Support g ; :: thesis: contradiction
HT p,T divides br by A6, TERMORD:1;
hence contradiction by A1, A8; :: thesis: verum

end;

A9: br is Element of Bags n by POLYNOM1:def 14;
A10: (f + g) . br = (f . br) + (g . br) by POLYNOM1:def 21
.= (f . br) + (0. L) by A7, A9, POLYNOM1:def 9
.= f . br by RLVECT_1:def 7 ;

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 23;
then (f + (- f)) + g = - f by POLYNOM1:80;
then (0_ n,L) + g = - f by POLYRED:3;
then g = - f by POLYRED:2;
hence contradiction by A5, A7, GROEB_1:5; :: thesis: verum

end;

case A11: 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 & br is Element of Bags n ) by A5, A10, POLYNOM1:def 9;
then br in Support (f + g) by POLYNOM1:def 9;
then f + g reduces_to (f + g) - ((((f + g) . br) / (HC p,T)) * (s *' p)),p,br,T by A5, A6, A11, POLYRED:def 5;
then A12: 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 A10, POLYNOM1:def 23
.= (f + (- (((f . br) / (HC p,T)) * (s *' p)))) + g by POLYNOM1:80
.= f1 + g by A6, POLYNOM1:def 23 ;
hence f + g reduces_to f1 + g,{p},T by A3, A12, POLYRED:def 7; :: thesis: verum

end;

end;

end;

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