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 :: thesis: ( ( not p is non-zero & term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) or ( p is non-zero & term (HM (p,O)) = HT (p,O) & coefficient (HM (p,O)) = HC (p,O) ) )

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 1;
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 12 ;
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;