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