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 p2,T <> 0. L by TERMORD:17;
then A4: not HC p2,T is zero by STRUCT_0:def 12;
A5: 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 ;
A6: p1 is non-zero by A2, POLYNOM7:def 2;
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 A7: Monom (HC p2,T),((lcm (HT p1,T),(HT p2,T)) / (HT p1,T)) is non-zero by POLYNOM7:def 2;
A8: 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 A6, A7, 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 ;
A9: HT p1,T divides lcm (HT p1,T),(HT p2,T) by Th7;
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 A6, A7, TERMORD:31
.= lcm (HT p1,T),(HT p2,T) by A9, A5, Def1 ;
A11: HC p1,T <> 0. L by A2, TERMORD:17;
then A12: not HC p1,T is zero by STRUCT_0:def 12;
A13: 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 A12, POLYNOM7:10 ;
A14: p2 is non-zero by A2, POLYNOM7:def 2;
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 A11, TERMORD:17;
then A15: Monom (HC p1,T),((lcm (HT p1,T),(HT p2,T)) / (HT p2,T)) is non-zero by POLYNOM7:def 2;
Support (S-Poly p1,p2,T) <> {} by A1, POLYNOM7:1;
then A16: HT (S-Poly p1,p2,T),T in Support (S-Poly p1,p2,T) by TERMORD:def 6;
A17: HT p2,T divides lcm (HT p1,T),(HT p2,T) by Th7;
A18: 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 A14, A15, 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 ;
A19: 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 A14, A15, TERMORD:31
.= lcm (HT p1,T),(HT p2,T) by A17, A13, Def1 ;
then (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 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, A19, 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 A8, A18, RLVECT_1:16 ;
then A20: not lcm (HT p1,T),(HT p2,T) in Support (S-Poly p1,p2,T) by POLYNOM1:def 9;
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 HT (S-Poly p1,p2,T),T <= lcm (HT p1,T),(HT p2,T),T by A10, A19, TERMORD:12;
hence HT (S-Poly p1,p2,T),T < lcm (HT p1,T),(HT p2,T),T by A16, A20, TERMORD:def 3; :: thesis: verum

end;

end;