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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 by Def6;
A2: p <> 0_ n,L by A1, Def5;
then A3: p is non-zero by POLYNOM7:def 2;
A4: HC p,T <> 0. L by A2, TERMORD:17;

A5: now

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

end;

b in Support f by A1, Def5;
then f . b <> 0. L by POLYNOM1:def 9;
then (f . b) * ((HC p,T) " ) <> 0. L by A5, VECTSP_2:def 5;
then (f . b) / (HC p,T) <> 0. L by VECTSP_1:def 23;
then A6: not (f . b) / (HC p,T) is zero by STRUCT_0:def 12;
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, Def5;
f = f + (0_ n,L) by POLYNOM1:82
.= f + ((m *' p) - (m *' p)) by POLYNOM1:83
.= f + ((m *' p) + (- (m *' p))) by POLYNOM1:def 23
.= (f + (- (m *' p))) + (m *' p) by POLYNOM1:80
.= (m *' p) + (f - (((f . b) / (HC p,T)) * (s *' p))) by A8, POLYNOM1:def 23 ;
then 0_ n,L = f - ((m *' p) + (f - (((f . b) / (HC p,T)) * (s *' p)))) by POLYNOM1:83
.= f + (- ((m *' p) + (f - (((f . b) / (HC p,T)) * (s *' p))))) by POLYNOM1:def 23
.= 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 23
.= 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 POLYNOM1:80
.= (f + (- f)) + ((- (m *' p)) + (((f . b) / (HC p,T)) * (s *' p))) by POLYNOM1:80
.= (f - f) + ((- (m *' p)) + (((f . b) / (HC p,T)) * (s *' p))) by POLYNOM1:def 23
.= (0_ n,L) + ((- (m *' p)) + (((f . b) / (HC p,T)) * (s *' p))) by POLYNOM1:83
.= (- (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:82
.= ((m *' p) + (- (m *' p))) + (((f . b) / (HC p,T)) * (s *' p)) by POLYNOM1:80
.= ((m *' p) - (m *' p)) + (((f . b) / (HC p,T)) * (s *' p)) by POLYNOM1:def 23
.= (0_ n,L) + (((f . b) / (HC p,T)) * (s *' p)) by POLYNOM1:83
.= ((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, Def5; :: thesis: verum