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 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; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: ( 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:87
.= ((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 ; :: thesis: 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:87
.= (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 ; :: thesis: verum