reconsider e = A --> 0 as Function of A,NAT by Th27;

defpred S_{1}[ 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_{1}[a] & S_{1}[b] holds

S_{1}[a [*] b]

_{1}[ 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_{1}[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_{3}(M) implies f " (NAT \ {0}) is finite )
:: thesis: ( f " (NAT \ {0}) is finite implies f in the carrier of M )

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

defpred S

( $1 = f & f " (NAT \ {0}) is finite );

A1: for a, b being Multiset of A st S

S

proof

A9:
dom e = A
;
let a, b be Multiset of A; :: thesis: ( S_{1}[a] & S_{1}[b] implies S_{1}[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_{1}[b] or S_{1}[a [*] b] )

given g being Function of A,NAT such that A4: b = g and

A5: g " (NAT \ {0}) is finite ; :: thesis: S_{1}[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}))

end;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

given g being Function of A,NAT such that A4: b = g and

A5: g " (NAT \ {0}) is finite ; :: thesis: S

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

hence
( a [*] b = h & h " (NAT \ {0}) is finite )
by A3, A5; :: thesis: verum
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;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

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

then A12:
Sset 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;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

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

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

proof

reconsider g = f as Function of A,NAT by Th27;
assume
f in H_{3}(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;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

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