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_{3}(M1) iff f " (NAT \ {0}) is finite )
and

A15: for f being Multiset of A holds

( f in H_{3}(M2) iff f " (NAT \ {0}) is finite )
; :: thesis: M1 = M2

A16: H_{3}(M2) c= H_{3}( MultiSet_over A)
by MONOID_0:23;

A17: H_{3}(M1) c= H_{3}( MultiSet_over A)
by MONOID_0:23;

H_{3}(M1) = H_{3}(M2)

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

A15: for f being Multiset of A holds

( f in H

A16: H

A17: H

H

proof

hence
M1 = M2
by MONOID_0:27; :: thesis: verum
thus
H_{3}(M1) c= H_{3}(M2)
:: according to XBOOLE_0:def 10 :: thesis: H_{3}(M2) c= H_{3}(M1)_{3}(M2) or x in H_{3}(M1) )

assume A19: x in H_{3}(M2)
; :: thesis: x in H_{3}(M1)

then reconsider f = x as Multiset of A by A16;

f " (NAT \ {0}) is finite by A15, A19;

hence x in H_{3}(M1)
by A14; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{3}(M1) or x in H_{3}(M2) )

assume A18: x in H_{3}(M1)
; :: thesis: x in H_{3}(M2)

then reconsider f = x as Multiset of A by A17;

f " (NAT \ {0}) is finite by A14, A18;

hence x in H_{3}(M2)
by A15; :: thesis: verum

end;assume A18: x in H

then reconsider f = x as Multiset of A by A17;

f " (NAT \ {0}) is finite by A14, A18;

hence x in H

assume A19: x in H

then reconsider f = x as Multiset of A by A16;

f " (NAT \ {0}) is finite by A15, A19;

hence x in H