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, g being Polynomial of n,L st f reduces_to g,p,T holds

ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )

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, g being Polynomial of n,L st f reduces_to g,p,T holds

ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )

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, g being Polynomial of n,L st f reduces_to g,p,T holds

ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )

let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T ) )

assume f reduces_to g,p,T ; :: thesis: ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),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: f . b <> 0. L by POLYNOM1:def 4;

p <> 0_ (n,L) by A1, POLYRED:def 5;

then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;

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;

set m = Monom (((f . b) / (HC (p,T))),s);

A5: (HC (p,T)) " <> 0. L by VECTSP_1:25;

A6: (f . b) / (HC (p,T)) <> 0. L by A2, A5, VECTSP_2:def 1;

then A7: not (f . b) / (HC (p,T)) is zero ;

coefficient (Monom (((f . b) / (HC (p,T))),s)) <> 0. L by A6, POLYNOM7:9;

then HC ((Monom (((f . b) / (HC (p,T))),s)),T) <> 0. L by TERMORD:23;

then Monom (((f . b) / (HC (p,T))),s) <> 0_ (n,L) by TERMORD:17;

then reconsider m = Monom (((f . b) / (HC (p,T))),s) as non-zero Monomial of n,L by POLYNOM7:def 1;

A8: HT ((m *' p),T) = (HT (m,T)) + (HT (p,T)) by TERMORD:31

.= (term m) + (HT (p,T)) by TERMORD:23

.= s + (HT (p,T)) by A7, POLYNOM7:10 ;

then HT ((m *' p),T) in Support f by A1, A3, POLYRED:def 5;

then ( ((f . b) / (HC (p,T))) * (s *' p) = (Monom (((f . b) / (HC (p,T))),s)) *' p & HT ((m *' p),T) <= HT (f,T),T ) by POLYRED:22, TERMORD:def 6;

hence ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T ) by A1, A3, A4, A8, POLYRED:39; :: thesis: verum

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, g being Polynomial of n,L st f reduces_to g,p,T holds

ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )

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, g being Polynomial of n,L st f reduces_to g,p,T holds

ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )

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, g being Polynomial of n,L st f reduces_to g,p,T holds

ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T )

let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T ) )

assume f reduces_to g,p,T ; :: thesis: ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),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: f . b <> 0. L by POLYNOM1:def 4;

p <> 0_ (n,L) by A1, POLYRED:def 5;

then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;

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;

set m = Monom (((f . b) / (HC (p,T))),s);

A5: (HC (p,T)) " <> 0. L by VECTSP_1:25;

A6: (f . b) / (HC (p,T)) <> 0. L by A2, A5, VECTSP_2:def 1;

then A7: not (f . b) / (HC (p,T)) is zero ;

coefficient (Monom (((f . b) / (HC (p,T))),s)) <> 0. L by A6, POLYNOM7:9;

then HC ((Monom (((f . b) / (HC (p,T))),s)),T) <> 0. L by TERMORD:23;

then Monom (((f . b) / (HC (p,T))),s) <> 0_ (n,L) by TERMORD:17;

then reconsider m = Monom (((f . b) / (HC (p,T))),s) as non-zero Monomial of n,L by POLYNOM7:def 1;

A8: HT ((m *' p),T) = (HT (m,T)) + (HT (p,T)) by TERMORD:31

.= (term m) + (HT (p,T)) by TERMORD:23

.= s + (HT (p,T)) by A7, POLYNOM7:10 ;

then HT ((m *' p),T) in Support f by A1, A3, POLYRED:def 5;

then ( ((f . b) / (HC (p,T))) * (s *' p) = (Monom (((f . b) / (HC (p,T))),s)) *' p & HT ((m *' p),T) <= HT (f,T),T ) by POLYRED:22, TERMORD:def 6;

hence ex m being Monomial of n,L st

( g = f - (m *' p) & not HT ((m *' p),T) in Support g & HT ((m *' p),T) <= HT (f,T),T ) by A1, A3, A4, A8, POLYRED:39; :: thesis: verum