for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A, B being LeftLinearCombination of P
for b being bag of n
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A /^ i & g = Sum (A | i) & i <= len A holds
B is_Standard_Representation_of f - g,P,b,T