let n be Ordinal; 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 p1, p2 being non-zero Polynomial of n,L st HT (p2,T) divides HT (p1,T) holds
(HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T
let T be 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 p1, p2 being non-zero Polynomial of n,L st HT (p2,T) divides HT (p1,T) holds
(HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; for p1, p2 being non-zero Polynomial of n,L st HT (p2,T) divides HT (p1,T) holds
(HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T
let p1, p2 be non-zero Polynomial of n,L; ( HT (p2,T) divides HT (p1,T) implies (HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T )
set hcp2 = HC (p2,T);
assume A1:
HT (p2,T) divides HT (p1,T)
; (HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T
then consider b being bag of n such that
A2:
HT (p1,T) = (HT (p2,T)) + b
by TERMORD:1;
set g = ((HC (p2,T)) * p1) - (((((HC (p2,T)) * p1) . (HT (p1,T))) / (HC (p2,T))) * (b *' p2));
A3:
p2 <> 0_ (n,L)
by POLYNOM7:def 1;
A4:
HC (p2,T) <> 0. L
;
p1 <> 0_ (n,L)
by POLYNOM7:def 1;
then
Support p1 <> {}
by POLYNOM7:1;
then A5:
HT (p1,T) in Support p1
by TERMORD:def 6;
A6:
Support p1 c= Support ((HC (p2,T)) * p1)
by POLYRED:20;
then
(HC (p2,T)) * p1 <> 0_ (n,L)
by A5, POLYNOM7:1;
then A7:
( HT (((HC (p2,T)) * p1),T) = HT (p1,T) & (HC (p2,T)) * p1 reduces_to ((HC (p2,T)) * p1) - (((((HC (p2,T)) * p1) . (HT (p1,T))) / (HC (p2,T))) * (b *' p2)),p2, HT (p1,T),T )
by A3, A5, A2, A6, POLYRED:21, POLYRED:def 5;
A8:
lcm ((HT (p1,T)),(HT (p2,T))) = HT (p1,T)
by A1, Th7;
((HC (p2,T)) * p1) - (((((HC (p2,T)) * p1) . (HT (p1,T))) / (HC (p2,T))) * (b *' p2)) =
((HC (p2,T)) * p1) - ((((HC (p2,T)) * (p1 . (HT (p1,T)))) / (HC (p2,T))) * (b *' p2))
by POLYNOM7:def 9
.=
((HC (p2,T)) * p1) - ((((HC (p2,T)) * (HC (p1,T))) / (HC (p2,T))) * (b *' p2))
by TERMORD:def 7
.=
((HC (p2,T)) * p1) - ((((HC (p2,T)) * (HC (p1,T))) * ((HC (p2,T)) ")) * (b *' p2))
.=
((HC (p2,T)) * p1) - (((HC (p1,T)) * ((HC (p2,T)) * ((HC (p2,T)) "))) * (b *' p2))
by GROUP_1:def 3
.=
((HC (p2,T)) * p1) - (((HC (p1,T)) * (1. L)) * (b *' p2))
by A4, VECTSP_1:def 10
.=
((HC (p2,T)) * p1) - ((HC (p1,T)) * (b *' p2))
.=
((HC (p2,T)) * ((EmptyBag n) *' p1)) - ((HC (p1,T)) * (b *' p2))
by POLYRED:17
.=
((HC (p2,T)) * (((HT (p1,T)) / (HT (p1,T))) *' p1)) - ((HC (p1,T)) * (b *' p2))
by Th6
.=
S-Poly (p1,p2,T)
by A1, A2, A8, Def1
;
hence
(HC (p2,T)) * p1 top_reduces_to S-Poly (p1,p2,T),p2,T
by A7, POLYRED:def 10; verum