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 6
.= 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 7; :: 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 9;
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 6 ;
:: thesis: ( HC m,O = coefficient m & HM m,O = m )
hence HC m,O = coefficient m by POLYNOM7:def 7; :: thesis: HM m,O = m
hence HM m,O = m by A6, POLYNOM7:11; :: thesis: verum

end;

end;