let n be Ordinal; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( Support (HM (p,O)) = {} or Support (HM (p,O)) = {(HT (p,O))} )
assume A1: not Support (HM (p,O)) = {} ; :: thesis: Support (HM (p,O)) = {(HT (p,O))}
then A2: ex b being bag of n st Support (HM (p,O)) = {b} by POLYNOM7:6;
now :: thesis: ( ( HC (p,O) = 0. L & Support (HM (p,O)) = {(HT (p,O))} ) or ( HC (p,O) <> 0. L & Support (HM (p,O)) = {(HT (p,O))} ) )
per cases ( HC (p,O) = 0. L or HC (p,O) <> 0. L ) ;
case HC (p,O) = 0. L ; :: thesis: Support (HM (p,O)) = {(HT (p,O))}
hence Support (HM (p,O)) = {(HT (p,O))} by A1, Lm10; :: thesis: verum
end;
case HC (p,O) <> 0. L ; :: thesis: Support (HM (p,O)) = {(HT (p,O))}
then HT (p,O) in Support (HM (p,O)) by Lm9;
hence Support (HM (p,O)) = {(HT (p,O))} by A2, TARSKI:def 1; :: thesis: verum
end;
end;
end;
hence Support (HM (p,O)) = {(HT (p,O))} ; :: thesis: verum