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