let n be Ordinal; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 2;
then A2:
HC g,T <> 0. L
by TERMORD:17;
A3:
f *' g <> 0_ n,L
by POLYNOM7:def 2;
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))
by VECTSP_1:def 23
.=
(f *' g) - (((HC f,T) * ((HC g,T) * ((HC g,T) " ))) * ((HT f,T) *' g))
by GROUP_1:def 4
.=
(f *' g) - (((HC f,T) * (1. L)) * ((HT f,T) *' g))
by A2, VECTSP_1:def 22
.=
(f *' g) - ((HC f,T) * ((HT f,T) *' g))
by VECTSP_1:def 16
.=
(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 23
.=
(f *' g) + (r *' g)
by POLYRED:6
.=
g *' (f + (- (HM f,T)))
by POLYNOM1:85
.=
(f - (HM f,T)) *' g
by POLYNOM1:def 23
.=
(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