for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g