theorem Th25: :: POLYNOM1:25

for n being set
for L being non empty right_unital multLoopStr_0 holds
( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L ) )