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
A12: for f being Multiset of A holds
( f in H₃(M1) iff f " (NAT \ {0 }) is finite ) and
A13: for f being Multiset of A holds
( f in H₃(M2) iff f " (NAT \ {0 }) is finite ) ; :: thesis: M1 = M2
set M = MultiSet_over A;
A14: ( H₃(M1) c= H₃( MultiSet_over A) & H₃(M2) c= H₃( MultiSet_over A) & H₃( MultiSet_over A) = Funcs A,NAT ) by Th27, MONOID_0:25;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in H₃(M1) or x in H₃(M2) )
assume A15: x in H₃(M1) ; :: thesis: x in H₃(M2)
then reconsider f = x as Multiset of A by A14;
f " (NAT \ {0 }) is finite by A12, A15;
hence x in H₃(M2) by A13; :: thesis: verum

end;

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

end;

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