reconsider e = A --> 0 as Function of A,NAT by Th27;
defpred S₁[ set ] means ex f being Function of A,NAT st
( $1 = f & f " (NAT \ {0}) is finite );
A1: for a, b being Multiset of A st S₁[a] & S₁[b] holds
S₁[a [*] b]

proof

let a, b be Multiset of A; :: thesis: ( S₁[a] & S₁[b] implies S₁[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 " (NAT \ {0}) is finite ; :: thesis: ( not S₁[b] or S₁[a [*] b] )
given g being Function of A,NAT such that A4: b = g and
A5: g " (NAT \ {0}) is finite ; :: thesis: S₁[a [*] b]
take h ; :: thesis: ( a [*] b = h & h " (NAT \ {0}) is finite )
A6: ( dom f = A & dom g = A ) by FUNCT_2:def 1;
h " (NAT \ {0}) c= (f " (NAT \ {0})) \/ (g " (NAT \ {0}))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in h " (NAT \ {0}) or x in (f " (NAT \ {0})) \/ (g " (NAT \ {0})) )
assume A7: x in h " (NAT \ {0}) ; :: thesis: x in (f " (NAT \ {0})) \/ (g " (NAT \ {0}))
then h . x in NAT \ {0} by FUNCT_1:def 7;
then A8: not h . x in {0} by XBOOLE_0:def 5;
( f . x in rng f & g . x in rng g ) by A6, A7, FUNCT_1:def 3;
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 A8, TARSKI:def 1;
then ( not n in {0} or not m in {0} ) by TARSKI:def 1;
then ( n in NAT \ {0} or m in NAT \ {0} ) by XBOOLE_0:def 5;
then ( x in f " (NAT \ {0}) or x in g " (NAT \ {0}) ) by A6, A7, FUNCT_1:def 7;
hence x in (f " (NAT \ {0})) \/ (g " (NAT \ {0})) by XBOOLE_0:def 3; :: thesis: verum

end;

hence ( a [*] b = h & h " (NAT \ {0}) is finite ) by A3, A5; :: thesis: verum

end;

A9: dom e = A ;

now :: thesis: not e " (NAT \ {0}) <> {}

set x = the Element of e " (NAT \ {0});
assume A10: e " (NAT \ {0}) <> {} ; :: thesis: contradiction
then e . the Element of e " (NAT \ {0}) in NAT \ {0} by FUNCT_1:def 7;
then A11: not e . the Element of e " (NAT \ {0}) in {0} by XBOOLE_0:def 5;
the Element of e " (NAT \ {0}) in A by A9, A10, FUNCT_1:def 7;
then e . the Element of e " (NAT \ {0}) = 0 by FUNCOP_1:7;
hence contradiction by A11, TARSKI:def 1; :: thesis: verum

end;

then A12: S₁[ 1. (MultiSet_over A)] 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 S₁[a] ) from MONOID_0:sch 2(A1, A12);
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 " (NAT \ {0}) is finite )
let f be Multiset of A; :: thesis: ( f in the carrier of M iff f " (NAT \ {0}) is finite )
thus ( f in H₃(M) implies f " (NAT \ {0}) is finite ) :: thesis: ( f " (NAT \ {0}) is finite implies f in the carrier of M )

proof

assume f in H₃(M) ; :: thesis: f " (NAT \ {0}) is finite
then ex g being Function of A,NAT st
( f = g & g " (NAT \ {0}) is finite ) by A13;
hence f " (NAT \ {0}) is finite ; :: thesis: verum

end;

reconsider g = f as Function of A,NAT by Th27;
assume f " (NAT \ {0}) is finite ; :: thesis: f in the carrier of M
then g " (NAT \ {0}) is finite ;
hence f in the carrier of M by A13; :: thesis: verum