:: deftheorem Def6 defines removed_last POLYNOM9:def 6 :
for n being Nat
for L being non empty ZeroStr
for p being Series of (n + 1),L
for b₄ being Series of n,L holds
( b₄ = p removed_last iff for b being bag of n holds b₄ . b = p . (b bag_extend 0) );