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 (Red (p1,T)) & b2 in Support (Red (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 (Red (p1,T)) & b2 in Support (Red (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 (Red (p1,T)) & b2 in Support (Red (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 (Red (p1,T)) & b2 in Support (Red (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 (Red (p1,T)) & b2 in Support (Red (p2,T)) holds
not (HT (p1,T)) + b2 = (HT (p2,T)) + b1
A2: ( Support (Red (p1,T)) c= Support p1 & Support (Red (p2,T)) c= Support p2 ) by TERMORD:35;
let b1, b2 be bag of n; :: thesis: ( b1 in Support (Red (p1,T)) & b2 in Support (Red (p2,T)) implies not (HT (p1,T)) + b2 = (HT (p2,T)) + b1 )
assume that
A3: b1 in Support (Red (p1,T)) and
A4: b2 in Support (Red (p2,T)) ; :: thesis: not (HT (p1,T)) + b2 = (HT (p2,T)) + b1

now :: thesis: not b1 = HT (p1,T)

assume b1 = HT (p1,T) ; :: thesis: contradiction
then (Red (p1,T)) . b1 = 0. L by TERMORD:39;
hence contradiction by A3, POLYNOM1:def 4; :: thesis: verum

end;

hence not (HT (p1,T)) + b2 = (HT (p2,T)) + b1 by A1, A3, A4, A2, Lm5; :: thesis: verum