set M = MultiSet_over A;
let M1, M2 be non empty strict MonoidalSubStr of MultiSet_over A; :: thesis: ( ( for f being Multiset of A holds
( f in the carrier of M1 iff f " (NAT \ {0}) is finite ) ) & ( for f being Multiset of A holds
( f in the carrier of M2 iff f " (NAT \ {0}) is finite ) ) implies M1 = M2 )
assume that
A14: for f being Multiset of A holds
( f in H3(M1) iff f " (NAT \ {0}) is finite ) and
A15: for f being Multiset of A holds
( f in H3(M2) iff f " (NAT \ {0}) is finite ) ; :: thesis: M1 = M2
A16: H3(M2) c= H3( MultiSet_over A) by MONOID_0:23;
A17: H3(M1) c= H3( MultiSet_over A) by MONOID_0:23;
H3(M1) = H3(M2)
proof
thus H3(M1) c= H3(M2) :: according to XBOOLE_0:def 10 :: thesis: H3(M2) c= H3(M1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H3(M1) or x in H3(M2) )
assume A18: x in H3(M1) ; :: thesis: x in H3(M2)
then reconsider f = x as Multiset of A by A17;
f " (NAT \ {0}) is finite by A14, A18;
hence x in H3(M2) by A15; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H3(M2) or x in H3(M1) )
assume A19: x in H3(M2) ; :: thesis: x in H3(M1)
then reconsider f = x as Multiset of A by A16;
f " (NAT \ {0}) is finite by A15, A19;
hence x in H3(M1) by A14; :: thesis: verum
end;
hence M1 = M2 by MONOID_0:27; :: thesis: verum