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 H₃(M1) iff f " (NAT \ {0}) is finite ) and
A15: for f being Multiset of A holds
( f in H₃(M2) iff f " (NAT \ {0}) is finite ) ; :: thesis: M1 = M2
A16: H₃(M2) c= H₃( MultiSet_over A) by MONOID_0:23;
A17: H₃(M1) c= H₃( MultiSet_over A) by MONOID_0:23;
H₃(M1) = H₃(M2)

proof

thus H₃(M1) c= H₃(M2) :: according to XBOOLE_0:def 10 :: thesis: H₃(M2) c= H₃(M1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₃(M1) or x in H₃(M2) )
assume A18: x in H₃(M1) ; :: thesis: x in H₃(M2)
then reconsider f = x as Multiset of A by A17;
f " (NAT \ {0}) is finite by A14, A18;
hence x in H₃(M2) by A15; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₃(M2) or x in H₃(M1) )
assume A19: x in H₃(M2) ; :: thesis: x in H₃(M1)
then reconsider f = x as Multiset of A by A16;
f " (NAT \ {0}) is finite by A15, A19;
hence x in H₃(M1) by A14; :: thesis: verum

end;

hence M1 = M2 by MONOID_0:27; :: thesis: verum