let n be Ordinal; :: thesis: for O being connected TermOrder of n
for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
let O be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
let L be non empty ZeroStr ; :: thesis: for m being Monomial of n,L holds
( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )
let m be Monomial of n,L; :: thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )

per cases ( Support m = {} or ex b being bag of n st Support m = {b} ) by POLYNOM7:6;

suppose A1: Support m = {} ; :: thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )

hence A2: term m = EmptyBag n by POLYNOM7:def 5
.= HT (m,O) by A1, Def6 ;
:: thesis: ( HC (m,O) = coefficient m & HM (m,O) = m )
hence HC (m,O) = coefficient m by POLYNOM7:def 6; :: thesis: HM (m,O) = m
hence HM (m,O) = m by A2, POLYNOM7:11; :: thesis: verum

end;

suppose A3: ex b being bag of n st Support m = {b} ; :: thesis: ( HT (m,O) = term m & HC (m,O) = coefficient m & HM (m,O) = m )

then consider b being bag of n such that
A4: Support m = {b} ;
b in Support m by A4, TARSKI:def 1;
then A5: m . b <> 0. L by POLYNOM1:def 4;
HT (m,O) in Support m by A3, Def6;
hence A6: HT (m,O) = b by A4, TARSKI:def 1
.= term m by A5, POLYNOM7:def 5 ;
:: thesis: ( HC (m,O) = coefficient m & HM (m,O) = m )
hence HC (m,O) = coefficient m by POLYNOM7:def 6; :: thesis: HM (m,O) = m
hence HM (m,O) = m by A6, POLYNOM7:11; :: thesis: verum

end;

end;