let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let p1, p2 be Polynomial of n,L; :: thesis:
assume A1: HT (p1,T), HT (p2,T) are_disjoint ; :: thesis:
then A2: S-Poly (p1,p2,T) = ((Red (p1,T)) *' p2) - ((Red (p2,T)) *' p1) by Th54;

now :: thesis:

per cases ;

case p1 = 0_ (n,L) ; :: thesis:

then ( (Red (p2,T)) *' p1 = 0_ (n,L) & Red (p1,T) = 0_ (n,L) ) by Th11, POLYNOM1:28;
then S-Poly (p1,p2,T) = (0_ (n,L)) - (0_ (n,L)) by A2, POLYNOM1:28
.= 0_ (n,L) by POLYRED:4 ;
hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) by REWRITE1:12; :: thesis:

end;

case p1 <> 0_ (n,L) ; :: thesis:

then reconsider p1a = p1 as non-zero Polynomial of n,L by POLYNOM7:def 1;

now :: thesis:

let u be object ; :: thesis:
assume u in {p2} ; :: thesis:
then u = p2 by TARSKI:def 1;
hence u in {p1,p2} by TARSKI:def 2; :: thesis:

end;

then A3: {p2} c= {p1,p2} ;
then A4: PolyRedRel ({p2},T) c= PolyRedRel ({p1,p2},T) by GROEB_1:4;

now :: thesis:

let u be object ; :: thesis:
assume u in {p1} ; :: thesis:
then u = p1 by TARSKI:def 1;
hence u in {p1,p2} by TARSKI:def 2; :: thesis:

end;

then A5: {p1} c= {p1,p2} ;
then A6: PolyRedRel ({p1},T) c= PolyRedRel ({p1,p2},T) by GROEB_1:4;

now :: thesis:

per cases ;

case p2 = 0_ (n,L) ; :: thesis:

then ( (Red (p1,T)) *' p2 = 0_ (n,L) & Red (p2,T) = 0_ (n,L) ) by Th11, POLYNOM1:28;
then S-Poly (p1,p2,T) = (0_ (n,L)) - (0_ (n,L)) by A2, POLYNOM1:28
.= 0_ (n,L) by POLYRED:4 ;
hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) by REWRITE1:12; :: thesis:

end;

case p2 <> 0_ (n,L) ; :: thesis:

then reconsider p2a = p2 as non-zero Polynomial of n,L by POLYNOM7:def 1;

now :: thesis:

per cases ;

case Red (p1,T) = 0_ (n,L) ; :: thesis:

then A7: S-Poly (p1,p2,T) = (0_ (n,L)) - ((Red (p2,T)) *' p1) by A2, POLYNOM1:28;

now :: thesis:

per cases ;

case Red (p2,T) = 0_ (n,L) ; :: thesis:

then S-Poly (p1,p2,T) = (0_ (n,L)) - (0_ (n,L)) by A7, POLYNOM1:28
.= 0_ (n,L) by POLYRED:4 ;
hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) by REWRITE1:12; :: thesis:

end;

case Red (p2,T) <> 0_ (n,L) ; :: thesis:

then reconsider rp2 = Red (p2,T) as non-zero Polynomial of n,L by POLYNOM7:def 1;
PolyRedRel ({p1a},T) reduces - (rp2 *' p1a), - (0_ (n,L)) by Th49, Th51;
then PolyRedRel ({p1a},T) reduces - (rp2 *' p1a), 0_ (n,L) by Th13;
then PolyRedRel ({p1},T) reduces S-Poly (p1,p2,T), 0_ (n,L) by A7, Th14;
hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) by A5, GROEB_1:4, REWRITE1:22; :: thesis:

end;

end;

end;

hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) ; :: thesis:

end;

case Red (p1,T) <> 0_ (n,L) ; :: thesis:

then reconsider rp1 = Red (p1,T) as non-zero Polynomial of n,L by POLYNOM7:def 1;

now :: thesis:

per cases ;

case Red (p2,T) = 0_ (n,L) ; :: thesis:

then (Red (p2,T)) *' p1 = 0_ (n,L) by POLYNOM1:28;
then A8: S-Poly (p1,p2,T) = ((Red (p1,T)) *' p2) - (0_ (n,L)) by A1, Th54
.= (Red (p1,T)) *' p2 by POLYRED:4 ;
PolyRedRel ({p2a},T) reduces rp1 *' p2a, 0_ (n,L) by Th51;
hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) by A3, A8, GROEB_1:4, REWRITE1:22; :: thesis:

end;

case Red (p2,T) <> 0_ (n,L) ; :: thesis:

then reconsider rp2 = Red (p2,T) as non-zero Polynomial of n,L by POLYNOM7:def 1;
S-Poly (p1,p2,T) = ((HM (p2a,T)) *' rp1) - ((HM (p1a,T)) *' rp2) by A1, Th53;
then A9: PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T),p2 *' (Red (p1,T)) by A1, A6, Th55, REWRITE1:22;
PolyRedRel ({p1,p2},T) reduces rp1 *' p2a, 0_ (n,L) by A4, Th51, REWRITE1:22;
hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) by A9, REWRITE1:16; :: thesis:

end;

end;

end;

hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) ; :: thesis:

end;

end;

end;

hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) ; :: thesis:

end;

end;

end;

hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) ; :: thesis:

end;

end;

end;

hence PolyRedRel ({p1,p2},T) reduces S-Poly (p1,p2,T), 0_ (n,L) ; :: thesis: