let x be set ; for A being non empty set st x is Element of (finite-MultiSet_over A) holds
ex p being FinSequence of A st x = |.p.|
let A be non empty set ; ( x is Element of (finite-MultiSet_over A) implies ex p being FinSequence of A st x = |.p.| )
defpred S1[ Nat] means for fm being Element of (finite-MultiSet_over A) st ( for V being finite set st V = fm " (NAT \ {0}) holds
card V = $1 ) holds
ex p being FinSequence of A st fm = |.p.|;
assume
x is Element of (finite-MultiSet_over A)
; ex p being FinSequence of A st x = |.p.|
then reconsider m = x as Element of (finite-MultiSet_over A) ;
H3( finite-MultiSet_over A) c= H3( MultiSet_over A)
by MONOID_0:23;
then
m is Multiset of A
;
then reconsider V = m " (NAT \ {0}) as finite set by Def6;
A1:
for V9 being finite set st V9 = m " (NAT \ {0}) holds
card V9 = card V
;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
deffunc H4(
object )
-> Element of
NAT =
0 ;
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
for
fm being
Element of
(finite-MultiSet_over A) st ( for
V being
finite set st
V = fm " (NAT \ {0}) holds
card V = n ) holds
ex
p being
FinSequence of
A st
fm = |.p.|
;
S1[n + 1]
let fm be
Element of
(finite-MultiSet_over A);
( ( for V being finite set st V = fm " (NAT \ {0}) holds
card V = n + 1 ) implies ex p being FinSequence of A st fm = |.p.| )
assume A4:
for
V being
finite set st
V = fm " (NAT \ {0}) holds
card V = n + 1
;
ex p being FinSequence of A st fm = |.p.|
deffunc H5(
object )
-> set =
fm . $1;
set x = the
Element of
fm " (NAT \ {0});
H3(
finite-MultiSet_over A)
c= H3(
MultiSet_over A)
by MONOID_0:23;
then reconsider m =
fm as
Multiset of
A ;
reconsider V =
m " (NAT \ {0}) as
finite set by Def6;
A5:
card V = n + 1
by A4;
A6:
dom m = A
by Th28;
then reconsider x = the
Element of
fm " (NAT \ {0}) as
Element of
A by A5, CARD_1:27, FUNCT_1:def 7;
defpred S2[
object ]
means x = $1;
consider f being
Function such that A7:
(
dom f = A & ( for
a being
object st
a in A holds
( (
S2[
a] implies
f . a = H4(
a) ) & ( not
S2[
a] implies
f . a = H5(
a) ) ) ) )
from PARTFUN1:sch 1();
rng f c= NAT
then reconsider f =
f as
Function of
A,
NAT by A7, FUNCT_2:def 1, RELSET_1:4;
reconsider f =
f as
Multiset of
A by Th27;
A10:
f " (NAT \ {0}) = (fm " (NAT \ {0})) \ {x}
then reconsider f9 =
f as
Element of
(finite-MultiSet_over A) by A5, Def6;
set g =
|.((m . x) .--> x).|;
A18:
card {x} = 1
by CARD_1:30;
reconsider V9 =
f9 " (NAT \ {0}) as
finite set by Def6;
{x} c= fm " (NAT \ {0})
by A5, CARD_1:27, ZFMISC_1:31;
then card V9 =
(n + 1) - 1
by A5, A10, A18, CARD_2:44
.=
n
;
then
for
V being
finite set st
V = f9 " (NAT \ {0}) holds
card V = n
;
then consider p being
FinSequence of
A such that A19:
f = |.p.|
by A3;
take q =
p ^ ((m . x) .--> x);
fm = |.q.|
hence fm =
f [*] |.((m . x) .--> x).|
by Th32
.=
|.q.|
by A19, Th40
;
verum
end;
A22:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A22, A2);
hence
ex p being FinSequence of A st x = |.p.|
by A1; verum