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₁[ 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: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 S₁[n] holds
S₁[n + 1]

proof

deffunc H₄( object ) -> Element of NAT = 0 ;
let n be 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₅( object ) -> set = fm . $1;
set x = the Element of fm " (NAT \ {0});
H₃( finite-MultiSet_over A) c= H₃( 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 S₂[ object ] means x = $1;
consider f being Function such that
A7: ( dom f = A & ( for a being object 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 object ; :: 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 object such that
A8: z in dom f and
A9: y = f . z by FUNCT_1:def 3;
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:4;
reconsider f = f as Multiset of A by Th27;
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 object ; :: 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 7;
A12: f . y in NAT \ {0} by A11, FUNCT_1:def 7;
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 7;
hence y in (fm " (NAT \ {0})) \ {x} by A14, XBOOLE_0:def 5; :: thesis: verum

end;

let y be object ; :: 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 7;
A17: fm . y in NAT \ {0} by A15, FUNCT_1:def 7;
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 7; :: 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: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); :: thesis: fm = |.q.|

now :: thesis: for a being Element of A holds (f [*] |.((m . x) .--> x).|) . a = m . a

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, Th41;
( f . x = 0 & |.((m . x) .--> x).| . x = m . x ) by A7, Th41;
hence (f [*] |.((m . x) .--> x).|) . a = m . a by A20, A21, Th29; :: thesis: verum

end;

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

end;

A22: S₁[ 0 ]

proof

set a = the 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:23;
then reconsider m = fm as Multiset of A ;
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:138;
then A24: {} = (rng fm) /\ (NAT \ {0})
.= ((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 Th28;
then A27: fm . the Element of A in rng fm by FUNCT_1:def 3;
then fm . the Element of A = 0 by A25, TARSKI:def 1;
then {0} c= rng fm by A27, ZFMISC_1:31;
then rng fm = {0} by A25;
hence fm = A --> 0 by A26, FUNCOP_1:9
.= |.p.| by Th37 ;
:: thesis: verum

end;

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