let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 n such that
A1: f reduces_to g,p,b,T by POLYRED:def 6;
b in Support f by A1, POLYRED:def 5;
then A2: b in Support (- f) by GROEB_1:5;
consider s being bag of n such that
A3: s + (HT (p,T)) = b and
A4: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A1, POLYRED:def 5;
g = f + (- (((f . b) / (HC (p,T))) * (s *' p))) by A4, POLYNOM1:def 7;
then A5: - g = (- f) + (- (- (((f . b) / (HC (p,T))) * (s *' p)))) by POLYRED:1
.= (- f) - (- (((f . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:def 7
.= (- f) - ((- ((f . b) / (HC (p,T)))) * (s *' p)) by POLYRED:9
.= (- f) - ((- ((f . b) * ((HC (p,T)) "))) * (s *' p))
.= (- f) - (((- (f . b)) * ((HC (p,T)) ")) * (s *' p)) by VECTSP_1:9
.= (- f) - (((- (f . b)) / (HC (p,T))) * (s *' p))
.= (- f) - ((((- f) . b) / (HC (p,T))) * (s *' p)) by POLYNOM1:17 ;

A6: now :: thesis: not - f = 0_ (n,L)

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

end;

p <> 0_ (n,L) by A1, POLYRED:def 5;
then - f reduces_to - g,p,b,T by A3, A6, A5, A2, POLYRED:def 5;
hence - f reduces_to - g,p,T by POLYRED:def 6; :: thesis: verum