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 add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
( b9 in Support g iff b9 in Support f )
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
( b9 in Support g iff b9 in Support f )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
( b9 in Support g iff b9 in Support f )
let f, p, g be Polynomial of n,L; :: thesis: for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
( b9 in Support g iff b9 in Support f )
let b, b9 be bag of n; :: thesis: ( b < b9,T & f reduces_to g,p,b,T implies ( b9 in Support g iff b9 in Support f ) )
assume A1: b < b9,T ; :: thesis: ( not f reduces_to g,p,b,T or ( b9 in Support g iff b9 in Support f ) )
assume f reduces_to g,p,b,T ; :: thesis: ( b9 in Support g iff b9 in Support f )
then consider s being bag of n such that
A2: s + (HT (p,T)) = b and
A3: g = f - (((f . b) / (HC (p,T))) * (s *' p)) ;
A4: b9 is Element of Bags n by PRE_POLY:def 12;

A5: now :: thesis: not b9 in Support (s *' p)

assume b9 in Support (s *' p) ; :: thesis: contradiction
then A6: b9 <= b,T by A2, Th16;
b <= b9,T by A1, TERMORD:def 3;
then b = b9 by A6, TERMORD:7;
hence contradiction by A1, TERMORD:def 3; :: thesis: verum

end;

A7: now :: thesis: ( b9 in Support f implies b9 in Support g )

A8: (((f . b) / (HC (p,T))) * (s *' p)) . b9 = ((f . b) / (HC (p,T))) * ((s *' p) . b9) by POLYNOM7:def 9
.= ((f . b) / (HC (p,T))) * (0. L) by A4, A5, POLYNOM1:def 4
.= 0. L ;
assume A9: b9 in Support f ; :: thesis: b9 in Support g
(f - (((f . b) / (HC (p,T))) * (s *' p))) . b9 = (f + (- (((f . b) / (HC (p,T))) * (s *' p)))) . b9 by POLYNOM1:def 7
.= (f . b9) + ((- (((f . b) / (HC (p,T))) * (s *' p))) . b9) by POLYNOM1:15
.= (f . b9) + (- (0. L)) by A8, POLYNOM1:17
.= (f . b9) + (0. L) by RLVECT_1:12
.= f . b9 by RLVECT_1:def 4 ;
then g . b9 <> 0. L by A3, A9, POLYNOM1:def 4;
hence b9 in Support g by A4, POLYNOM1:def 4; :: thesis: verum

end;

now :: thesis: ( b9 in Support g implies b9 in Support f )

A10: (((f . b) / (HC (p,T))) * (s *' p)) . b9 = ((f . b) / (HC (p,T))) * ((s *' p) . b9) by POLYNOM7:def 9
.= ((f . b) / (HC (p,T))) * (0. L) by A4, A5, POLYNOM1:def 4
.= 0. L ;
assume A11: b9 in Support g ; :: thesis: b9 in Support f
(f - (((f . b) / (HC (p,T))) * (s *' p))) . b9 = (f + (- (((f . b) / (HC (p,T))) * (s *' p)))) . b9 by POLYNOM1:def 7
.= (f . b9) + ((- (((f . b) / (HC (p,T))) * (s *' p))) . b9) by POLYNOM1:15
.= (f . b9) + (- (0. L)) by A10, POLYNOM1:17
.= (f . b9) + (0. L) by RLVECT_1:12
.= f . b9 by RLVECT_1:def 4 ;
then f . b9 <> 0. L by A3, A11, POLYNOM1:def 4;
hence b9 in Support f by A4, POLYNOM1:def 4; :: thesis: verum

end;

hence ( b9 in Support g iff b9 in Support f ) by A7; :: thesis: verum