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 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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:87
.= (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:83 ; :: 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:87
.= ((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:83 ; :: 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 by STRUCT_0:def 12;
HC m1,T <> 0. L by A5, TERMORD:17;
then A7: not HC m1,T is zero by STRUCT_0:def 12;
A8: HT m2,T divides lcm (HT m1,T),(HT m2,T) by Th7;
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 Th7;
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:83; :: thesis: verum

end;

end;