theorem Th30: :: MONOID_1:30

for X, Y being set holds chi (Y,X) is Multiset of X