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

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)

hence
not (HT (p1,T)) + b2 = (HT (p2,T)) + b1
by A1, A3, A4, A2, Lm5; :: thesis: verumassume
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;then (Red (p1,T)) . b1 = 0. L by TERMORD:39;

hence contradiction by A3, POLYNOM1:def 4; :: thesis: verum