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, g, p being Polynomial of n,L st f reduces_to g,p,T holds
- f reduces_to - 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, g, p being Polynomial of n,L st f reduces_to g,p,T holds
- f reduces_to - 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, g, p being Polynomial of n,L st f reduces_to g,p,T holds
- f reduces_to - g,p,T
let f, g, p be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies - f reduces_to - g,p,T )
assume f reduces_to g,p,T ; :: thesis: - f reduces_to - g,p,T
then consider b being bag of such that
A1: f reduces_to g,p,b,T by POLYRED:def 6;
A2: ( f <> 0_ n,L & p <> 0_ n,L & b in Support f & ex s being bag of st
( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) ) by A1, POLYRED:def 5;
consider s being bag of such that
A3: ( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) by A1, POLYRED:def 5;

A4: now

assume - f = 0_ n,L ; :: thesis: contradiction
then f = - (0_ n,L)
.= 0_ n,L by Th13 ;
hence contradiction by A1, POLYRED:def 5; :: thesis: verum

end;

g = f + (- (((f . b) / (HC p,T)) * (s *' p))) by A3, POLYNOM1:def 23;
then - g = (- f) + (- (- (((f . b) / (HC p,T)) * (s *' p)))) by POLYRED:1
.= (- f) - (- (((f . b) / (HC p,T)) * (s *' p))) by POLYNOM1:def 23
.= (- f) - ((- ((f . b) / (HC p,T))) * (s *' p)) by POLYRED:9
.= (- f) - ((- ((f . b) * ((HC p,T) " ))) * (s *' p)) by VECTSP_1:def 23
.= (- f) - (((- (f . b)) * ((HC p,T) " )) * (s *' p)) by VECTSP_1:41
.= (- f) - (((- (f . b)) / (HC p,T)) * (s *' p)) by VECTSP_1:def 23
.= (- f) - ((((- f) . b) / (HC p,T)) * (s *' p)) by POLYNOM1:def 22 ;
then ( - f <> 0_ n,L & p <> 0_ n,L & b in Support (- f) & ex s being bag of st
( s + (HT p,T) = b & - g = (- f) - ((((- f) . b) / (HC p,T)) * (s *' p)) ) ) by A2, A3, A4, GROEB_1:5;
then - f reduces_to - g,p,b,T by POLYRED:def 5;
hence - f reduces_to - g,p,T by POLYRED:def 6; :: thesis: verum