for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being non-zero Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds
ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )