let X be set ; :: thesis: for L being non empty ZeroStr
for m being Monomial of X,L holds
( Support m = {} or Support m = {(term m)} )
let L be non empty ZeroStr ; :: thesis: for m being Monomial of X,L holds
( Support m = {} or Support m = {(term m)} )
let m be Monomial of X,L; :: thesis: ( Support m = {} or Support m = {(term m)} )
assume A1: Support m <> {} ; :: thesis: Support m = {(term m)}
then consider b being bag of such that
A2: Support m = {b} by Th6;
A3: m . (term m) <> 0. L by A1, Def6;
term m is Element of Bags X by POLYNOM1:def 14;
then term m in Support m by A3, POLYNOM1:def 9;
hence Support m = {(term m)} by A2, TARSKI:def 1; :: thesis: verum