let n be Ordinal; :: thesis: for T being connected 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 st f reduces_to g,p,T holds

ex m being Monomial of n,L st g = f - (m *' p)

let T be connected 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 st f reduces_to g,p,T holds

ex m being Monomial of n,L st g = f - (m *' p)

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 st f reduces_to g,p,T holds

ex m being Monomial of n,L st g = f - (m *' p)

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) )

assume f reduces_to g,p,T ; :: thesis: ex m being Monomial of n,L st g = f - (m *' p)

then consider b being bag of n such that

A1: f reduces_to g,p,b,T by POLYRED:def 6;

consider s being bag of n such that

s + (HT (p,T)) = b and

A2: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A1, POLYRED:def 5;

((f . b) / (HC (p,T))) * (s *' p) = (Monom (((f . b) / (HC (p,T))),s)) *' p by POLYRED:22;

hence ex m being Monomial of n,L st g = f - (m *' p) by A2; :: thesis: verum

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 st f reduces_to g,p,T holds

ex m being Monomial of n,L st g = f - (m *' p)

let T be connected 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 st f reduces_to g,p,T holds

ex m being Monomial of n,L st g = f - (m *' p)

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 st f reduces_to g,p,T holds

ex m being Monomial of n,L st g = f - (m *' p)

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) )

assume f reduces_to g,p,T ; :: thesis: ex m being Monomial of n,L st g = f - (m *' p)

then consider b being bag of n such that

A1: f reduces_to g,p,b,T by POLYRED:def 6;

consider s being bag of n such that

s + (HT (p,T)) = b and

A2: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A1, POLYRED:def 5;

((f . b) / (HC (p,T))) * (s *' p) = (Monom (((f . b) / (HC (p,T))),s)) *' p by POLYRED:22;

hence ex m being Monomial of n,L st g = f - (m *' p) by A2; :: thesis: verum