reconsider e = A --> 0 as Function of A,NAT by Th28;
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 Th28;
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 set ; :: 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 13;
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 5;
then reconsider n = f . x, m = g . x as Element of NAT ;
h . x = n + m by A2, A4, A7, Th30;
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 13;
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 by FUNCOP_1:19;

now

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

end;

then A12: S₁[ 1. (MultiSet_over A)] by Th27;
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 Th28;
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