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_{1}[ 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_{3}( finite-MultiSet_over A) c= H_{3}( 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A22, A2);

hence ex p being FinSequence of A st x = |.p.| by A1; :: thesis: verum

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

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

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

S

proof

A22:
S
deffunc H_{4}( object ) -> Element of NAT = 0 ;

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[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_{1}[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_{5}( object ) -> set = fm . $1;

set x = the Element of fm " (NAT \ {0});

H_{3}( finite-MultiSet_over A) c= H_{3}( 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_{2}[ object ] means x = $1;

consider f being Function such that

A7: ( dom f = A & ( for a being object st a in A holds

( ( S_{2}[a] implies f . a = H_{4}(a) ) & ( not S_{2}[a] implies f . a = H_{5}(a) ) ) ) )
from PARTFUN1:sch 1();

rng f c= NAT

reconsider f = f as Multiset of A by Th27;

A10: f " (NAT \ {0}) = (fm " (NAT \ {0})) \ {x}

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.|

.= |.q.| by A19, Th40 ;

:: thesis: verum

end;let n be Nat; :: thesis: ( S

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

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 x = the Element of fm " (NAT \ {0});

H

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

consider f being Function such that

A7: ( dom f = A & ( for a being object st a in A holds

( ( S

rng f c= NAT

proof

then reconsider f = f as Function of A,NAT by A7, FUNCT_2:def 1, RELSET_1:4;
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;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

reconsider f = f as Multiset of A by Th27;

A10: f " (NAT \ {0}) = (fm " (NAT \ {0})) \ {x}

proof

then reconsider f9 = f as Element of (finite-MultiSet_over A) by A5, Def6;
thus
f " (NAT \ {0}) c= (fm " (NAT \ {0})) \ {x}
:: according to XBOOLE_0:def 10 :: thesis: (fm " (NAT \ {0})) \ {x} c= 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;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (fm " (NAT \ {0})) \ {x} or y in f " (NAT \ {0}) )
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;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

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

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

hence fm =
f [*] |.((m . x) .--> x).|
by Th32
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;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

.= |.q.| by A19, Th40 ;

:: thesis: verum

proof

for n being Nat holds S
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_{3}( finite-MultiSet_over A) c= H_{3}( 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;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

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

hence ex p being FinSequence of A st x = |.p.| by A1; :: thesis: verum