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 st HT p1,T, HT p2,T are_disjoint holds
for b1, b2 being bag of n st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
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 st HT p1,T, HT p2,T are_disjoint holds
for b1, b2 being bag of n st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
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 st HT p1,T, HT p2,T are_disjoint holds
for b1, b2 being bag of n st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
let p1, p2 be Polynomial of n,L; :: thesis: ( HT p1,T, HT p2,T are_disjoint implies for b1, b2 being bag of n st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1 )
assume A1: HT p1,T, HT p2,T are_disjoint ; :: thesis: for b1, b2 being bag of n st b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) holds
not (HT p1,T) + b2 = (HT p2,T) + b1
let b1, b2 be bag of n; :: thesis: ( b1 in Support p1 & b2 in Support p2 & ( not b1 = HT p1,T or not b2 = HT p2,T ) implies not (HT p1,T) + b2 = (HT p2,T) + b1 )
assume that
A2: b1 in Support p1 and
A3: b2 in Support p2 ; :: thesis: ( ( b1 = HT p1,T & b2 = HT p2,T ) or not (HT p1,T) + b2 = (HT p2,T) + b1 )
assume A4: ( not b1 = HT p1,T or not b2 = HT p2,T ) ; :: thesis: not (HT p1,T) + b2 = (HT p2,T) + b1
b2 <= HT p2,T,T by A3, TERMORD:def 6;
then A5: (HT p1,T) + b2 <= (HT p1,T) + (HT p2,T),T by Th2;
b1 <= HT p1,T,T by A2, TERMORD:def 6;
then A6: (HT p2,T) + b1 <= (HT p1,T) + (HT p2,T),T by Th2;
assume A7: (HT p1,T) + b2 = (HT p2,T) + b1 ; :: thesis: contradiction
then A8: HT p1,T divides (HT p2,T) + b1 by PRE_POLY:50;
A9: HT p2,T divides (HT p1,T) + b2 by A7, PRE_POLY:50;

now

per cases ( not b1 = HT p1,T or not b2 = HT p2,T ) by A4;

case A10: not b1 = HT p1,T ; :: thesis: contradiction

HT p2,T divides (HT p2,T) + b1 by PRE_POLY:50;
then lcm (HT p1,T),(HT p2,T) divides (HT p2,T) + b1 by A8, GROEB_2:8;
then (HT p1,T) + (HT p2,T) divides (HT p2,T) + b1 by A1, GROEB_2:9;
then (HT p1,T) + (HT p2,T) <= (HT p2,T) + b1,T by TERMORD:10;
then A11: (HT p1,T) + (HT p2,T) = (HT p2,T) + b1 by A6, TERMORD:7;
HT p1,T = ((HT p1,T) + (HT p2,T)) -' (HT p2,T) by PRE_POLY:48;
hence contradiction by A10, A11, PRE_POLY:48; :: thesis: verum

end;

case A12: not b2 = HT p2,T ; :: thesis: contradiction

HT p1,T divides (HT p1,T) + b2 by PRE_POLY:50;
then lcm (HT p1,T),(HT p2,T) divides (HT p1,T) + b2 by A9, GROEB_2:8;
then (HT p1,T) + (HT p2,T) divides (HT p1,T) + b2 by A1, GROEB_2:9;
then (HT p1,T) + (HT p2,T) <= (HT p1,T) + b2,T by TERMORD:10;
then A13: (HT p1,T) + (HT p2,T) = (HT p1,T) + b2 by A5, TERMORD:7;
HT p2,T = ((HT p1,T) + (HT p2,T)) -' (HT p1,T) by PRE_POLY:48;
hence contradiction by A12, A13, PRE_POLY:48; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum