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] )
given f being Function of A, NAT such that A2: ( a = f & f " (NAT \ {0 }) is finite ) ; :: thesis: ( not S₁[b] or S₁[a [*] b] )
given g being Function of A, NAT such that A3: ( b = g & g " (NAT \ {0 }) is finite ) ; :: thesis: S₁[a [*] b]
reconsider h = a [*] b as Function of A, NAT by Th28;
take h ; :: thesis: ( a [*] b = h & h " (NAT \ {0 }) is finite )
A4: (f " (NAT \ {0 })) \/ (g " (NAT \ {0 })) is finite by A2, A3;
A5: ( dom h = A & dom f = A & dom g = A & rng f c= NAT & rng g c= NAT ) 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 A6: x in h " (NAT \ {0 }) ; :: thesis: x in (f " (NAT \ {0 })) \/ (g " (NAT \ {0 }))
then A7: ( x in A & h . x in NAT \ {0 } ) by FUNCT_1:def 13;
( f . x in rng f & g . x in rng g ) by A5, A6, FUNCT_1:def 5;
then reconsider n = f . x, m = g . x as Element of NAT ;
( h . x = n + m & not h . x in {0 } ) by A2, A3, A7, Th30, XBOOLE_0:def 5;
then ( n <> 0 or m <> 0 ) by 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 A5, A6, 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 A4; :: thesis: verum

end;

reconsider e = A --> 0 as Function of A, NAT by Th28;
A8: ( dom e = A & rng e c= {0 } & {0 } c= NAT ) by FUNCOP_1:19;

A9: now

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

end;

e = H₂( MultiSet_over A) by Th27;
then A10: S₁[ 1. (MultiSet_over A)] by A9;
consider M being non empty strict MonoidalSubStr of MultiSet_over A such that
A11: for a being Multiset of A holds
( a in the carrier of M iff S₁[a] ) from MONOID_0:sch 4(A1, A10);
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 )
reconsider g = f as Function of A, NAT by Th28;
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 A11;
hence f " (NAT \ {0 }) is finite ; :: thesis: verum

end;

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 A11; :: thesis: verum