let x be set ; :: thesis: for A being non empty set st x is Element of holds
ex p being FinSequence of A st x = |.p.|

let A be non empty set ; :: thesis: ( x is Element of implies ex p being FinSequence of A st x = |.p.| )
defpred S1[ Nat] means for fm being Element of st ( for V being finite set st V = fm " () holds
card V = \$1 ) holds
ex p being FinSequence of A st fm = |.p.|;
assume x is Element of ; :: thesis: ex p being FinSequence of A st x = |.p.|
then reconsider m = x as Element of ;
H3( finite-MultiSet_over A) c= H3( MultiSet_over A) by MONOID_0:23;
then m is Multiset of A ;
then reconsider V = m " () as finite set by Def6;
A1: for V9 being finite set st V9 = m " () 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; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: for fm being Element of st ( for V being finite set st V = fm " () holds
card V = n ) holds
ex p being FinSequence of A st fm = |.p.| ; :: thesis: S1[n + 1]
let fm be Element of ; :: thesis: ( ( for V being finite set st V = fm " () 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 " () holds
card V = n + 1 ; :: thesis: ex p being FinSequence of A st fm = |.p.|
deffunc H5( object ) -> set = fm . \$1;
set x = the Element of fm " ();
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 " () 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 " () as Element of A by ;
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 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:
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 ;
reconsider f = f as Multiset of A by Th27;
A10: f " () = (fm " ()) \ {x}
proof
thus f " () c= (fm " ()) \ {x} :: according to XBOOLE_0:def 10 :: thesis: (fm " ()) \ {x} c= f " ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f " () or y in (fm " ()) \ {x} )
assume A11: y in f " () ; :: thesis: y in (fm " ()) \ {x}
then reconsider a = y as Element of A by ;
A12: f . y in NAT \ by ;
then not f . a in 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 ;
then a in fm " () by ;
hence y in (fm " ()) \ {x} by ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (fm " ()) \ {x} or y in f " () )
assume A15: y in (fm " ()) \ {x} ; :: thesis: y in f " ()
then A16: y in dom fm by FUNCT_1:def 7;
A17: fm . y in NAT \ by ;
not y in {x} by ;
then y <> x by TARSKI:def 1;
then fm . y = f . y by A6, A7, A16;
hence y in f " () by ; :: thesis: verum
end;
then reconsider f9 = f as Element of by ;
set g = |.((m . x) .--> x).|;
A18: card {x} = 1 by CARD_1:30;
reconsider V9 = f9 " () as finite set by Def6;
{x} c= fm " () by ;
then card V9 = (n + 1) - 1 by
.= n ;
then for V being finite set st V = f9 " () 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 ;
( f . x = 0 & |.((m . x) .--> x).| . x = m . x ) by ;
hence (f [*] |.((m . x) .--> x).|) . a = m . a by ; :: thesis: verum
end;
hence fm = f [*] |.((m . x) .--> x).| by Th32
.= |.q.| by ;
:: thesis: verum
end;
A22: S1[ 0 ]
proof
set a = the Element of A;
let fm be Element of ; :: thesis: ( ( for V being finite set st V = fm " () holds
card V = 0 ) implies ex p being FinSequence of A st fm = |.p.| )

assume A23: for V being finite set st V = fm " () holds
card V = 0 ; :: thesis: ex p being FinSequence of A st fm = |.p.|
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 " () as finite set by Def6;
card V = 0 by A23;
then fm " () = {} ;
then rng fm misses NAT \ by RELAT_1:138;
then A24: {} = (rng fm) /\ ()
.= ((rng fm) /\ NAT) \ 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= by ;
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 ;
then {0} c= rng fm by ;
then rng fm = by A25;
hence fm = A --> 0 by
.= |.p.| by Th37 ;
:: thesis: verum
end;
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; :: thesis: verum