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)} )
A1: term m is Element of Bags X by PRE_POLY:def 12;
assume A2: Support m <> {} ; :: thesis: Support m = {(term m)}
then m . (term m) <> 0. L by Def5;
then A3: term m in Support m by A1, POLYNOM1:def 4;
ex b being bag of X st Support m = {b} by A2, Th6;
hence Support m = {(term m)} by A3, TARSKI:def 1; :: thesis: verum