let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( term (HM p,T) = HT p,T & coefficient (HM p,T) = HC p,T )
let O be connected TermOrder of n; :: thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O )
let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of n,L holds
( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O )
let p be Polynomial of n,L; :: thesis: ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O )

per cases ( not HC p,O is zero or HC p,O is zero ) ;

suppose not HC p,O is zero ; :: thesis: ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O )

then reconsider a = HC p,O as non zero Element of L ;
term (Monom a,(HT p,O)) = HT p,O by POLYNOM7:10;
hence ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O ) by POLYNOM7:9; :: thesis: verum

end;

suppose A1: HC p,O is zero ; :: thesis: ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O )

now

per cases ( not p is non-zero or p is non-zero ) ;

case not p is non-zero ; :: thesis: ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O )

then p = 0_ n,L by POLYNOM7:def 2;
then Support p = {} by POLYNOM7:1;
then HT p,O = EmptyBag n by Def6
.= term (Monom (0. L),(HT p,O)) by POLYNOM7:8
.= term (HM p,O) by A1, STRUCT_0:def 15 ;
hence ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O ) by POLYNOM7:9; :: thesis: verum

end;

case p is non-zero ; :: thesis: ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O )

then reconsider p = p as non-zero Polynomial of n,L ;
not HC p,O is zero ;
hence ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O ) by A1; :: thesis: verum

end;

end;

end;

hence ( term (HM p,O) = HT p,O & coefficient (HM p,O) = HC p,O ) ; :: thesis: verum

end;

end;