theorem :: PRE_POLY:73

for n being Ordinal holds decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*>