let n be Ordinal; for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
let O be connected TermOrder of n; for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
let L be non trivial ZeroStr ; for p being Polynomial of n,L holds
( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
let p be Polynomial of n,L; ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
assume A1:
not Support (HM (p,O)) = {}
; Support (HM (p,O)) = {(HT (p,O))}
then A2:
ex b being bag of n st Support (HM (p,O)) = {b}
by POLYNOM7:6;
hence
Support (HM (p,O)) = {(HT (p,O))}
; verum