theorem Th2: :: FUNCTOR0:2

for I being set
for M being ManySortedSet of I holds M * (id I) = M