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

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