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