let a be object ; :: thesis: for I being set holds
( a is multiset of I iff a is bag of I )
let I be set ; :: thesis: ( a is multiset of I iff a is bag of I )
thus ( a is multiset of I implies a is bag of I ) ; :: thesis: ( a is bag of I implies a is multiset of I )
assume a is bag of I ; :: thesis: a is multiset of I
then reconsider b = a as bag of I ;
( dom b = I & rng b c= NAT ) by PARTFUN1:def 2, VALUED_0:def 6;
then b is Function of I,NAT by FUNCT_2:2;
then ( b is Multiset of I & support b is finite ) by MONOID_1:27;
hence a is multiset of I by MONOID_1:def 6; :: thesis: verum