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 n 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 n 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 n 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 n st [(HT (p,T)),b] in T & b <> HT (p,T) holds
p . b = 0. L
let b be bag of n; :: 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 :: thesis: not b in Support p

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:4; :: thesis: verum

end;

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