let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, p being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds
HT ((m *' p),T) in Support f
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, p being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds
HT ((m *' p),T) in Support f
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, p being Polynomial of n,L
for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds
HT ((m *' p),T) in Support f
let f, p be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L st f reduces_to f - (m *' p),p,T holds
HT ((m *' p),T) in Support f
let m be non-zero Monomial of n,L; :: thesis: ( f reduces_to f - (m *' p),p,T implies HT ((m *' p),T) in Support f )
assume f reduces_to f - (m *' p),p,T ; :: thesis: HT ((m *' p),T) in Support f
then consider b being bag of n such that
A1: f reduces_to f - (m *' p),p,b,T ;
A2: p <> 0_ (n,L) by A1;
then A3: p is non-zero ;
A4: HC (p,T) <> 0. L by A2, TERMORD:17;

A5: now :: thesis: not (HC (p,T)) " = 0. L

assume (HC (p,T)) " = 0. L ; :: thesis: contradiction
then 0. L = (HC (p,T)) * ((HC (p,T)) ")
.= 1. L by A4, VECTSP_1:def 10 ;
hence contradiction ; :: thesis: verum

end;

b in Support f by A1;
then f . b <> 0. L by POLYNOM1:def 4;
then (f . b) * ((HC (p,T)) ") <> 0. L by A5, VECTSP_2:def 1;
then (f . b) / (HC (p,T)) <> 0. L ;
then A6: not (f . b) / (HC (p,T)) is zero ;
consider s being bag of n such that
A7: s + (HT (p,T)) = b and
A8: f - (m *' p) = f - (((f . b) / (HC (p,T))) * (s *' p)) by A1;
A9: ((f . b) / (HC (p,T))) * (s *' p) = - (- (((f . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:19;
f = f + (0_ (n,L)) by POLYNOM1:23
.= f + ((m *' p) - (m *' p)) by POLYNOM1:24
.= f + ((m *' p) + (- (m *' p))) by POLYNOM1:def 7
.= (f + (- (m *' p))) + (m *' p) by POLYNOM1:21
.= (m *' p) + (f - (((f . b) / (HC (p,T))) * (s *' p))) by A8, POLYNOM1:def 7 ;
then 0_ (n,L) = f - ((m *' p) + (f - (((f . b) / (HC (p,T))) * (s *' p)))) by POLYNOM1:24
.= f + (- ((m *' p) + (f - (((f . b) / (HC (p,T))) * (s *' p))))) by POLYNOM1:def 7
.= f + ((- (m *' p)) + (- (f - (((f . b) / (HC (p,T))) * (s *' p))))) by Th1
.= f + ((- (m *' p)) + (- (f + (- (((f . b) / (HC (p,T))) * (s *' p)))))) by POLYNOM1:def 7
.= f + ((- (m *' p)) + ((- f) + (- (- (((f . b) / (HC (p,T))) * (s *' p)))))) by Th1
.= f + ((- f) + ((- (m *' p)) + (((f . b) / (HC (p,T))) * (s *' p)))) by A9, POLYNOM1:21
.= (f + (- f)) + ((- (m *' p)) + (((f . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:21
.= (f - f) + ((- (m *' p)) + (((f . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:def 7
.= (0_ (n,L)) + ((- (m *' p)) + (((f . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:24
.= (- (m *' p)) + (((f . b) / (HC (p,T))) * (s *' p)) by Th2 ;
then m *' p = (m *' p) + ((- (m *' p)) + (((f . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:23
.= ((m *' p) + (- (m *' p))) + (((f . b) / (HC (p,T))) * (s *' p)) by POLYNOM1:21
.= ((m *' p) - (m *' p)) + (((f . b) / (HC (p,T))) * (s *' p)) by POLYNOM1:def 7
.= (0_ (n,L)) + (((f . b) / (HC (p,T))) * (s *' p)) by POLYNOM1:24
.= ((f . b) / (HC (p,T))) * (s *' p) by Th2 ;
then HT ((m *' p),T) = HT ((s *' p),T) by A6, Th21
.= b by A7, A3, Th15 ;
hence HT ((m *' p),T) in Support f by A1; :: thesis: verum