let A be non empty set ; :: thesis: for p being FinSequence of A holds |.p.| is Element of (finite-MultiSet_over A)
let p be FinSequence of A; :: thesis: |.p.| is Element of (finite-MultiSet_over A)
defpred S1[ FinSequence of A] means |.$1.| is Element of (finite-MultiSet_over A);
defpred S2[ Nat] means for p being FinSequence of A st len p = $1 holds
S1[p];
A1: len p = len p ;
A2: for n being Nat st S2[n] holds
S2[n + 1]
proof
set M = finite-MultiSet_over A;
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A3: for p being FinSequence of A st len p = n holds
S1[p] ; :: thesis: S2[n + 1]
let p be FinSequence of A; :: thesis: ( len p = n + 1 implies S1[p] )
assume A4: len p = n + 1 ; :: thesis: S1[p]
then p <> {} ;
then consider r being FinSequence, x being object such that
A5: p = r ^ <*x*> by FINSEQ_1:46;
rng <*x*> = {x} by FINSEQ_1:39;
then {x} c= rng p by A5, FINSEQ_1:30;
then A6: {x} c= A by XBOOLE_1:1;
reconsider r = r as FinSequence of A by A5, FINSEQ_1:36;
A7: len <*x*> = 1 by FINSEQ_1:40;
reconsider x = x as Element of A by A6, ZFMISC_1:31;
n + 1 = (len r) + 1 by A4, A5, A7, FINSEQ_1:22;
then reconsider r9 = |.r.|, a = chi x as Element of (finite-MultiSet_over A) by A3, Th33;
finite-MultiSet_over A is SubStr of MultiSet_over A by MONOID_0:21;
then r9 [*] a = |.r.| [*] (chi x) by MONOID_0:25
.= |.p.| by A5, Th39 ;
hence S1[p] ; :: thesis: verum
end;
A8: S2[ 0 ]
proof
let p be FinSequence of A; :: thesis: ( len p = 0 implies S1[p] )
assume len p = 0 ; :: thesis: S1[p]
then p = <*> A ;
then |.p.| = A --> 0 by Th37
.= H2( MultiSet_over A) by Th26
.= H2( finite-MultiSet_over A) by MONOID_0:def 24 ;
hence S1[p] ; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A8, A2);
 hence |.p.| is Element of (finite-MultiSet_over A) by A1; :: thesis: verum