let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of st [(HT p,T),b] in T & b <> HT p,T holds
p . b = 0. L
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of st [(HT p,T),b] in T & b <> HT p,T holds
p . b = 0. L
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L
for b being bag of st [(HT p,T),b] in T & b <> HT p,T holds
p . b = 0. L
let p be Polynomial of n,L; :: thesis: for b being bag of st [(HT p,T),b] in T & b <> HT p,T holds
p . b = 0. L
let b be bag of ; :: thesis: ( [(HT p,T),b] in T & b <> HT p,T implies p . b = 0. L )
A1: b is Element of Bags n by PRE_POLY:def 12;
assume A2: ( [(HT p,T),b] in T & b <> HT p,T ) ; :: thesis: p . b = 0. L

now

assume b in Support p ; :: thesis: contradiction
then b <= HT p,T,T by TERMORD:def 6;
then [b,(HT p,T)] in T by TERMORD:def 2;
hence contradiction by A2, A1, ORDERS_1:13; :: thesis: verum

end;

hence p . b = 0. L by A1, POLYNOM1:def 9; :: thesis: verum