\b1 b2 e -> unionbag (unionbag b1 (singletonbag e)) b2

===[use assoc/comm                               (step 1)

\b1 b2 e -> unionbag (unionbag (singletonbag e) b1) b2

===[apply catalog bag.thy                        (step 2)

\b1 b2 e -> nonemptybag e (unionbag b1 b2)