let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 such that
A1: f reduces_to g,p,b,T by POLYRED:def 6;
consider s being bag of such that
A2: ( s + (HT p,T) = b & 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