let n be Ordinal; :: thesis: 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 m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for m1, m2 being Monomial of n,L holds S-Poly (m1,m2,T) = 0_ (n,L)
let m1, m2 be Monomial of n,L; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)
per cases ( m1 = 0_ (n,L) or m2 = 0_ (n,L) or ( m1 <> 0_ (n,L) & m2 <> 0_ (n,L) ) ) ;
suppose A1: m1 = 0_ (n,L) ; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)
A2: HC ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))),T) = coefficient (Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) by TERMORD:23
.= HC ((0_ (n,L)),T) by POLYNOM7:9
.= 0. L by TERMORD:17 ;
thus S-Poly (m1,m2,T) = ((Monom ((HC (m2,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' (0_ (n,L))) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2)) by
.= (0_ (n,L)) - ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2)) by POLYNOM1:28
.= (0_ (n,L)) - ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' m2) by POLYRED:22
.= (0_ (n,L)) - ((0_ (n,L)) *' m2) by
.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5
.= 0_ (n,L) by POLYNOM1:24 ; :: thesis: verum
end;
suppose A3: m2 = 0_ (n,L) ; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)
A4: HC ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))),T) = coefficient (Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) by TERMORD:23
.= HC ((0_ (n,L)),T) by POLYNOM7:9
.= 0. L by TERMORD:17 ;
thus S-Poly (m1,m2,T) = ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1)) - ((Monom ((HC (m1,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' (0_ (n,L))) by
.= ((HC ((0_ (n,L)),T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1)) - (0_ (n,L)) by POLYNOM1:28
.= ((Monom ((HC ((0_ (n,L)),T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' m1) - (0_ (n,L)) by POLYRED:22
.= ((0_ (n,L)) *' m1) - (0_ (n,L)) by
.= (0_ (n,L)) - (0_ (n,L)) by POLYRED:5
.= 0_ (n,L) by POLYNOM1:24 ; :: thesis: verum
end;
suppose A5: ( m1 <> 0_ (n,L) & m2 <> 0_ (n,L) ) ; :: thesis: S-Poly (m1,m2,T) = 0_ (n,L)
then HC (m2,T) <> 0. L by TERMORD:17;
then A6: not HC (m2,T) is zero ;
HC (m1,T) <> 0. L by ;
then A7: not HC (m1,T) is zero ;
A8: HT (m2,T) divides lcm ((HT (m1,T)),(HT (m2,T))) by Th3;
A9: m2 = Monom ((),(term m2)) by POLYNOM7:11
.= Monom ((HC (m2,T)),(term m2)) by TERMORD:23
.= Monom ((HC (m2,T)),(HT (m2,T))) by TERMORD:23 ;
A10: HT (m1,T) divides lcm ((HT (m1,T)),(HT (m2,T))) by Th3;
A11: m1 = Monom ((),(term m1)) by POLYNOM7:11
.= Monom ((HC (m1,T)),(term m1)) by TERMORD:23
.= Monom ((HC (m1,T)),(HT (m1,T))) by TERMORD:23 ;
A12: (HC (m1,T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) *' m2) = (Monom ((HC (m1,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))))) *' m2 by POLYRED:22
.= Monom (((HC (m2,T)) * (HC (m1,T))),(((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m2,T))) + (HT (m2,T)))) by
.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by ;
(HC (m2,T)) * (((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) *' m1) = (Monom ((HC (m2,T)),((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))))) *' m1 by POLYRED:22
.= Monom (((HC (m2,T)) * (HC (m1,T))),(((lcm ((HT (m1,T)),(HT (m2,T)))) / (HT (m1,T))) + (HT (m1,T)))) by
.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by ;
hence S-Poly (m1,m2,T) = 0_ (n,L) by ; :: thesis: verum
end;
end;