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 p being Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
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 p being Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; for p being Polynomial of n,L holds
( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
let p be Polynomial of n,L; ( S-Poly (p,(0_ (n,L)),T) = 0_ (n,L) & S-Poly ((0_ (n,L)),p,T) = 0_ (n,L) )
set p2 = 0_ (n,L);
thus S-Poly (p,(0_ (n,L)),T) =
((HC ((0_ (n,L)),T)) * (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - ((Monom ((HC (p,T)),((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT ((0_ (n,L)),T))))) *' (0_ (n,L)))
by POLYRED:22
.=
((HC ((0_ (n,L)),T)) * (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L))
by POLYNOM1:28
.=
((0. L) * (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L))
by TERMORD:17
.=
(((0. L) | (n,L)) *' (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L))
by POLYNOM7:27
.=
((0_ (n,L)) *' (((lcm ((HT (p,T)),(HT ((0_ (n,L)),T)))) / (HT (p,T))) *' p)) - (0_ (n,L))
by POLYNOM7:19
.=
(0_ (n,L)) - (0_ (n,L))
by POLYRED:5
.=
0_ (n,L)
by POLYRED:4
; S-Poly ((0_ (n,L)),p,T) = 0_ (n,L)
thus S-Poly ((0_ (n,L)),p,T) =
((Monom ((HC (p,T)),((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT ((0_ (n,L)),T))))) *' (0_ (n,L))) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p))
by POLYRED:22
.=
(0_ (n,L)) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p))
by POLYNOM1:28
.=
(0_ (n,L)) - ((0. L) * (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p))
by TERMORD:17
.=
(0_ (n,L)) - (((0. L) | (n,L)) *' (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p))
by POLYNOM7:27
.=
(0_ (n,L)) - ((0_ (n,L)) *' (((lcm ((HT ((0_ (n,L)),T)),(HT (p,T)))) / (HT (p,T))) *' p))
by POLYNOM7:19
.=
(0_ (n,L)) - (0_ (n,L))
by POLYRED:5
.=
0_ (n,L)
by POLYRED:4
; verum