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

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