reconsider e = A --> 0 as Function of A,NAT by Th27;
defpred S1[ set ] means ex f being Function of A,NAT st
( \$1 = f & f " () is finite );
A1: for a, b being Multiset of A st S1[a] & S1[b] holds
S1[a [*] b]
proof
let a, b be Multiset of A; :: thesis: ( S1[a] & S1[b] implies S1[a [*] b] )
reconsider h = a [*] b as Function of A,NAT by Th27;
given f being Function of A,NAT such that A2: a = f and
A3: f " () is finite ; :: thesis: ( not S1[b] or S1[a [*] b] )
given g being Function of A,NAT such that A4: b = g and
A5: g " () is finite ; :: thesis: S1[a [*] b]
take h ; :: thesis: ( a [*] b = h & h " () is finite )
A6: ( dom f = A & dom g = A ) by FUNCT_2:def 1;
h " () c= (f " ()) \/ (g " ())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in h " () or x in (f " ()) \/ (g " ()) )
assume A7: x in h " () ; :: thesis: x in (f " ()) \/ (g " ())
then h . x in NAT \ by FUNCT_1:def 7;
then A8: not h . x in by XBOOLE_0:def 5;
( f . x in rng f & g . x in rng g ) by ;
then reconsider n = f . x, m = g . x as Element of NAT ;
h . x = n + m by A2, A4, A7, Th29;
then ( n <> 0 or m <> 0 ) by ;
then ( not n in or not m in ) by TARSKI:def 1;
then ( n in NAT \ or m in NAT \ ) by XBOOLE_0:def 5;
then ( x in f " () or x in g " () ) by ;
hence x in (f " ()) \/ (g " ()) by XBOOLE_0:def 3; :: thesis: verum
end;
hence ( a [*] b = h & h " () is finite ) by A3, A5; :: thesis: verum
end;
A9: dom e = A ;
now :: thesis: not e " () <> {}
set x = the Element of e " ();
assume A10: e " () <> {} ; :: thesis: contradiction
then e . the Element of e " () in NAT \ by FUNCT_1:def 7;
then A11: not e . the Element of e " () in by XBOOLE_0:def 5;
the Element of e " () in A by ;
then e . the Element of e " () = 0 by FUNCOP_1:7;
hence contradiction by A11, TARSKI:def 1; :: thesis: verum
end;
then A12: S1[ 1. ()] by Th26;
consider M being non empty strict MonoidalSubStr of MultiSet_over A such that
A13: for a being Multiset of A holds
( a in the carrier of M iff S1[a] ) from reconsider M = M as non empty strict MonoidalSubStr of MultiSet_over A ;
take M ; :: thesis: for f being Multiset of A holds
( f in the carrier of M iff f " () is finite )

let f be Multiset of A; :: thesis: ( f in the carrier of M iff f " () is finite )
thus ( f in H3(M) implies f " () is finite ) :: thesis: ( f " () is finite implies f in the carrier of M )
proof
assume f in H3(M) ; :: thesis: f " () is finite
then ex g being Function of A,NAT st
( f = g & g " () is finite ) by A13;
hence f " () is finite ; :: thesis: verum
end;
reconsider g = f as Function of A,NAT by Th27;
assume f " () is finite ; :: thesis: f in the carrier of M
then g " () is finite ;
hence f in the carrier of M by A13; :: thesis: verum