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 A1, POLYRED:22
.= (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 A2, TERMORD:17
.= (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 A3, POLYRED:22
.= ((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 A4, TERMORD:17
.= (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 A5, TERMORD:17;
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 ((coefficient m2),(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 ((coefficient m1),(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 A7, A6, A9, TERMORD:3
.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by A8, Def1 ;
(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 A7, A6, A11, TERMORD:3
.= Monom (((HC (m2,T)) * (HC (m1,T))),(lcm ((HT (m1,T)),(HT (m2,T))))) by A10, Def1 ;
hence S-Poly (m1,m2,T) = 0_ (n,L) by A12, POLYNOM1:24; :: thesis: verum

end;

end;