let x be set ; :: thesis: 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 ; :: thesis: ( x is Element of (finite-MultiSet_over A) implies ex p being FinSequence of A st x = |.p.| )
defpred S₁[ Element of 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) ; :: thesis: ex p being FinSequence of A st x = |.p.|
then reconsider m = x as Element of (finite-MultiSet_over A) ;
H₃( finite-MultiSet_over A) c= H₃( MultiSet_over A) by MONOID_0:25;
then m is Multiset of A by TARSKI:def 3;
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 Element of NAT st S₁[n] holds
S₁[n + 1]

proof

deffunc H₄( set ) -> Element of NAT = 0 ;
let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[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.| ; :: thesis: S₁[n + 1]
let fm be Element of (finite-MultiSet_over A); :: thesis: ( ( 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 ; :: thesis: ex p being FinSequence of A st fm = |.p.|
deffunc H₅( set ) -> set = fm . $1;
consider x being Element of fm " (NAT \ {0});
H₃( finite-MultiSet_over A) c= H₃( MultiSet_over A) by MONOID_0:25;
then reconsider m = fm as Multiset of A by TARSKI:def 3;
reconsider V = m " (NAT \ {0}) as finite set by Def6;
A5: card V = n + 1 by A4;
A6: dom m = A by Th29;
then reconsider x = x as Element of A by A5, CARD_1:47, FUNCT_1:def 13;
defpred S₂[ set ] means x = $1;
consider f being Function such that
A7: ( dom f = A & ( for a being set st a in A holds
( ( S₂[a] implies f . a = H₄(a) ) & ( not S₂[a] implies f . a = H₅(a) ) ) ) ) from PARTFUN1:sch 1();
rng f c= NAT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider z being set such that
A8: z in dom f and
A9: y = f . z by FUNCT_1:def 5;
reconsider z = z as Element of A by A7, A8;
( y = 0 or y = m . z ) by A7, A9;
hence y in NAT ; :: thesis: verum

end;

then reconsider f = f as Function of A,NAT by A7, FUNCT_2:def 1, RELSET_1:11;
reconsider f = f as Multiset of A by Th28;
A10: f " (NAT \ {0}) = (fm " (NAT \ {0})) \ {x}

proof

thus f " (NAT \ {0}) c= (fm " (NAT \ {0})) \ {x} :: according to XBOOLE_0:def 10 :: thesis: (fm " (NAT \ {0})) \ {x} c= f " (NAT \ {0})

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f " (NAT \ {0}) or y in (fm " (NAT \ {0})) \ {x} )
assume A11: y in f " (NAT \ {0}) ; :: thesis: y in (fm " (NAT \ {0})) \ {x}
then reconsider a = y as Element of A by A7, FUNCT_1:def 13;
A12: f . y in NAT \ {0} by A11, FUNCT_1:def 13;
then not f . a in {0} by XBOOLE_0:def 5;
then A13: f . a <> 0 by TARSKI:def 1;
then a <> x by A7;
then A14: not a in {x} by TARSKI:def 1;
f . a = fm . a by A7, A13;
then a in fm " (NAT \ {0}) by A6, A12, FUNCT_1:def 13;
hence y in (fm " (NAT \ {0})) \ {x} by A14, XBOOLE_0:def 5; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (fm " (NAT \ {0})) \ {x} or y in f " (NAT \ {0}) )
assume A15: y in (fm " (NAT \ {0})) \ {x} ; :: thesis: y in f " (NAT \ {0})
then A16: y in dom fm by FUNCT_1:def 13;
A17: fm . y in NAT \ {0} by A15, FUNCT_1:def 13;
not y in {x} by A15, XBOOLE_0:def 5;
then y <> x by TARSKI:def 1;
then fm . y = f . y by A6, A7, A16;
hence y in f " (NAT \ {0}) by A6, A7, A16, A17, FUNCT_1:def 13; :: thesis: verum

end;

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:50;
reconsider V9 = f9 " (NAT \ {0}) as finite set by Def6;
{x} c= fm " (NAT \ {0}) by A5, CARD_1:47, ZFMISC_1:37;
then card V9 = (n + 1) - 1 by A5, A10, A18, CARD_2:63
.= 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); :: thesis: fm = |.q.|

now

let a be Element of A; :: thesis: (f [*] |.((m . x) .--> x).|) . a = m . a
A20: 0 + (m . a) = m . a ;
A21: ( a <> x implies ( f . a = m . a & |.((m . x) .--> x).| . a = 0 ) ) by A7, Th42;
( f . x = 0 & |.((m . x) .--> x).| . x = m . x ) by A7, Th42;
hence (f [*] |.((m . x) .--> x).|) . a = m . a by A20, A21, Th30; :: thesis: verum

end;

hence fm = f [*] |.((m . x) .--> x).| by Th33
.= |.q.| by A19, Th41 ;
:: thesis: verum

end;

A22: S₁[ 0 ]

proof

consider a being Element of A;
let fm be Element of (finite-MultiSet_over A); :: thesis: ( ( for V being finite set st V = fm " (NAT \ {0}) holds
card V = 0 ) implies ex p being FinSequence of A st fm = |.p.| )
assume A23: for V being finite set st V = fm " (NAT \ {0}) holds
card V = 0 ; :: thesis: ex p being FinSequence of A st fm = |.p.|
H₃( finite-MultiSet_over A) c= H₃( MultiSet_over A) by MONOID_0:25;
then reconsider m = fm as Multiset of A by TARSKI:def 3;
reconsider V = m " (NAT \ {0}) as finite set by Def6;
card V = 0 by A23;
then fm " (NAT \ {0}) = {} ;
then rng fm misses NAT \ {0} by RELAT_1:173;
then A24: {} = (rng fm) /\ (NAT \ {0}) by XBOOLE_0:def 7
.= ((rng fm) /\ NAT) \ {0} by XBOOLE_1:49 ;
take p = <*> A; :: thesis: fm = |.p.|
rng m c= NAT ;
then (rng fm) /\ NAT = rng fm by XBOOLE_1:28;
then A25: rng fm c= {0} by A24, XBOOLE_1:37;
A26: dom m = A by Th29;
then A27: fm . a in rng fm by FUNCT_1:def 5;
then fm . a = 0 by A25, TARSKI:def 1;
then {0} c= rng fm by A27, ZFMISC_1:37;
then rng fm = {0} by A25, XBOOLE_0:def 10;
hence fm = A --> 0 by A26, FUNCOP_1:15
.= |.p.| by Th38 ;
:: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A22, A2);
hence ex p being FinSequence of A st x = |.p.| by A1; :: thesis: verum