for X being set
for L being non empty multLoopStr_0
for a being Element of L holds
( (a | (X,L)) . (EmptyBag X) = a & ( for b being bag of X st b <> EmptyBag X holds
(a | (X,L)) . b = 0. L ) )