let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for a being Element of L holds
( HT ((a | (n,L)),T) = EmptyBag n & HC ((a | (n,L)),T) = a )
let O be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for a being Element of L holds
( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a )
let L be non empty ZeroStr ; :: thesis: for a being Element of L holds
( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a )
let a be Element of L; :: thesis: ( HT ((a | (n,L)),O) = EmptyBag n & HC ((a | (n,L)),O) = a )
set p = a | (n,L);
thus HT ((a | (n,L)),O) = term (a | (n,L)) by Lm11
.= EmptyBag n by POLYNOM7:23 ; :: thesis: HC ((a | (n,L)),O) = a
thus HC ((a | (n,L)),O) = coefficient (a | (n,L)) by Lm11
.= a by POLYNOM7:23 ; :: thesis: verum