let n be Ordinal; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red (f,T)) *' g,{g},T
let T be connected admissible TermOrder of n; for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red (f,T)) *' g,{g},T
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for f, g being non-zero Polynomial of n,L holds f *' g reduces_to (Red (f,T)) *' g,{g},T
let f, g be non-zero Polynomial of n,L; f *' g reduces_to (Red (f,T)) *' g,{g},T
set fg = f *' g;
set q = (f *' g) - ((((f *' g) . (HT ((f *' g),T))) / (HC (g,T))) * ((HT (f,T)) *' g));
reconsider r = - (HM (f,T)) as Polynomial of n,L ;
A1:
g <> 0_ (n,L)
by POLYNOM7:def 1;
A2:
HC (g,T) <> 0. L
;
A3:
f *' g <> 0_ (n,L)
by POLYNOM7:def 1;
then
Support (f *' g) <> {}
by POLYNOM7:1;
then A4:
HT ((f *' g),T) in Support (f *' g)
by TERMORD:def 6;
HT ((f *' g),T) = (HT (f,T)) + (HT (g,T))
by TERMORD:31;
then
f *' g reduces_to (f *' g) - ((((f *' g) . (HT ((f *' g),T))) / (HC (g,T))) * ((HT (f,T)) *' g)),g, HT ((f *' g),T),T
by A3, A1, A4, POLYRED:def 5;
then A5:
( g in {g} & f *' g reduces_to (f *' g) - ((((f *' g) . (HT ((f *' g),T))) / (HC (g,T))) * ((HT (f,T)) *' g)),g,T )
by POLYRED:def 6, TARSKI:def 1;
(f *' g) - ((((f *' g) . (HT ((f *' g),T))) / (HC (g,T))) * ((HT (f,T)) *' g)) =
(f *' g) - (((HC ((f *' g),T)) / (HC (g,T))) * ((HT (f,T)) *' g))
by TERMORD:def 7
.=
(f *' g) - ((((HC (f,T)) * (HC (g,T))) / (HC (g,T))) * ((HT (f,T)) *' g))
by TERMORD:32
.=
(f *' g) - ((((HC (f,T)) * (HC (g,T))) * ((HC (g,T)) ")) * ((HT (f,T)) *' g))
.=
(f *' g) - (((HC (f,T)) * ((HC (g,T)) * ((HC (g,T)) "))) * ((HT (f,T)) *' g))
by GROUP_1:def 3
.=
(f *' g) - (((HC (f,T)) * (1. L)) * ((HT (f,T)) *' g))
by A2, VECTSP_1:def 10
.=
(f *' g) - ((HC (f,T)) * ((HT (f,T)) *' g))
.=
(f *' g) - ((Monom ((HC (f,T)),(HT (f,T)))) *' g)
by POLYRED:22
.=
(f *' g) - ((HM (f,T)) *' g)
by TERMORD:def 8
.=
(f *' g) + (- ((HM (f,T)) *' g))
by POLYNOM1:def 7
.=
(f *' g) + (r *' g)
by POLYRED:6
.=
g *' (f + (- (HM (f,T))))
by POLYNOM1:26
.=
(f - (HM (f,T))) *' g
by POLYNOM1:def 7
.=
(Red (f,T)) *' g
by TERMORD:def 9
;
hence
f *' g reduces_to (Red (f,T)) *' g,{g},T
by A5, POLYRED:def 7; verum