for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L holds (EmptyBag n) *' p = p