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 (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 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 (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 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 (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

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

end;

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