let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( HT (c,T) = EmptyBag n & HC (c,T) = c . (EmptyBag n) )
let O be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) )
let L be non empty ZeroStr ; :: thesis: for c being ConstPoly of n,L holds
( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) )
let c be ConstPoly of n,L; :: thesis: ( HT (c,O) = EmptyBag n & HC (c,O) = c . (EmptyBag n) )
thus HT (c,O) = term c by Lm11
.= EmptyBag n by POLYNOM7:16 ; :: thesis: HC (c,O) = c . (EmptyBag n)
thus HC (c,O) = coefficient c by Lm11
.= c . (EmptyBag n) by POLYNOM7:16 ; :: thesis: verum