let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of n,L holds
( S-Poly p1,p2,T = 0_ n,L or HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T )
let T be connected admissible 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 p1, p2 being Polynomial of n,L holds
( S-Poly p1,p2,T = 0_ n,L or HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T )
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of n,L holds
( S-Poly p1,p2,T = 0_ n,L or HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T )
let p1, p2 be Polynomial of n,L; :: thesis: ( S-Poly p1,p2,T = 0_ n,L or HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T )
assume A1: S-Poly p1,p2,T <> 0_ n,L ; :: thesis: HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T
set sp = S-Poly p1,p2,T;
set g1 = (HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1);
set g2 = (HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2);

per cases ( p1 = 0_ n,L or p2 = 0_ n,L or ( p1 <> 0_ n,L & p2 <> 0_ n,L ) ) ;

suppose ( p1 = 0_ n,L or p2 = 0_ n,L ) ; :: thesis: HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T

hence HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T by A1, Th25; :: thesis: verum

end;

suppose A2: ( p1 <> 0_ n,L & p2 <> 0_ n,L ) ; :: thesis: HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T

then A3: ( HC p1,T <> 0. L & HC p2,T <> 0. L ) by TERMORD:17;
then A4: ( not HC p1,T is zero & not HC p2,T is zero ) by STRUCT_0:def 15;
A5: HT p1,T divides lcm (HT p1,T),(HT p2,T) by Th7;
A6: HT p2,T divides lcm (HT p1,T),(HT p2,T) by Th7;
A7: ( p1 is non-zero & p2 is non-zero ) by A2, POLYNOM7:def 2;
A8: HT (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))),T = term (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) by TERMORD:23
.= (lcm (HT p1,T),(HT p2,T)) / (HT p1,T) by A4, POLYNOM7:10 ;
HC (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))),T = coefficient (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) by TERMORD:23
.= HC p2,T by POLYNOM7:9 ;
then Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) <> 0_ n,L by A3, TERMORD:17;
then A9: Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) is non-zero by POLYNOM7:def 2;
A10: HT ((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)),T = HT ((Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) *' p1),T by POLYRED:22
.= (HT (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))),T) + (HT p1,T) by A7, A9, TERMORD:31
.= lcm (HT p1,T),(HT p2,T) by A5, A8, Def1 ;
A11: HT (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))),T = term (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) by TERMORD:23
.= (lcm (HT p1,T),(HT p2,T)) / (HT p2,T) by A4, POLYNOM7:10 ;
HC (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))),T = coefficient (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) by TERMORD:23
.= HC p1,T by POLYNOM7:9 ;
then Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) <> 0_ n,L by A3, TERMORD:17;
then A12: Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) is non-zero by POLYNOM7:def 2;
A13: HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T = HT ((Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) *' p2),T by POLYRED:22
.= (HT (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))),T) + (HT p2,T) by A7, A12, TERMORD:31
.= lcm (HT p1,T),(HT p2,T) by A6, A11, Def1 ;
HT (S-Poly p1,p2,T),T <= max (HT ((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)),T),(HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T),T,T by GROEB_1:7;
then A14: HT (S-Poly p1,p2,T),T <= lcm (HT p1,T),(HT p2,T),T by A10, A13, TERMORD:12;
A15: HC ((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)),T = HC ((Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))) *' p1),T by POLYRED:22
.= (HC (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T))),T) * (HC p1,T) by A7, A9, TERMORD:32
.= (coefficient (Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)))) * (HC p1,T) by TERMORD:23
.= (HC p1,T) * (HC p2,T) by POLYNOM7:9 ;
A16: HC ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T = HC ((Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))) *' p2),T by POLYRED:22
.= (HC (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T))),T) * (HC p2,T) by A7, A12, TERMORD:32
.= (coefficient (Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)))) * (HC p2,T) by TERMORD:23
.= (HC p1,T) * (HC p2,T) by POLYNOM7:9 ;
Support (S-Poly p1,p2,T) <> {} by A1, POLYNOM7:1;
then A17: HT (S-Poly p1,p2,T),T in Support (S-Poly p1,p2,T) by TERMORD:def 6;
(S-Poly p1,p2,T) . (lcm (HT p1,T),(HT p2,T)) = (((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)) + (- ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)))) . (HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T) by A13, POLYNOM1:def 23
.= (((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)) . (HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T)) + ((- ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2))) . (HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T)) by POLYNOM1:def 21
.= (((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)) . (HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T)) + (- (((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)) . (HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T))) by POLYNOM1:def 22
.= (HC ((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)),T) + (- (((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)) . (HT ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T))) by A10, A13, TERMORD:def 7
.= (HC ((HC p2,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) *' p1)),T) + (- (HC ((HC p1,T) * (((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) *' p2)),T)) by TERMORD:def 7
.= 0. L by A15, A16, RLVECT_1:16 ;
then not lcm (HT p1,T),(HT p2,T) in Support (S-Poly p1,p2,T) by POLYNOM1:def 9;
hence HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T by A14, A17, TERMORD:def 3; :: thesis: verum

end;

end;