let n be Ordinal; 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; 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 ; 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; ( 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
; HC ((a | (n,L)),O) = a
thus HC ((a | (n,L)),O) =
coefficient (a | (n,L))
by Lm11
.=
a
by POLYNOM7:23
; verum