let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 :: thesis: ( ( not b1 = HT (p1,T) & contradiction ) or ( not b2 = HT (p2,T) & contradiction ) )

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:4;
then (HT (p1,T)) + (HT (p2,T)) divides (HT (p2,T)) + b1 by A1, GROEB_2:5;
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:4;
then (HT (p1,T)) + (HT (p2,T)) divides (HT (p1,T)) + b2 by A1, GROEB_2:5;
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