let X be set ; :: thesis: for L being non empty ZeroStr
for c being ConstPoly of X,L holds
( Support c = {} or Support c = {(EmptyBag X)} )
let L be non empty ZeroStr ; :: thesis: for c being ConstPoly of X,L holds
( Support c = {} or Support c = {(EmptyBag X)} )
let c be ConstPoly of X,L; :: thesis: ( Support c = {} or Support c = {(EmptyBag X)} )
assume Support c <> {} ; :: thesis: Support c = {(EmptyBag X)}
hence Support c = {(term c)} by Th7
.= {(EmptyBag X)} by Lm2 ;
:: thesis: verum