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 S₁[ FinSequence of A] means |.$1.| is Element of (finite-MultiSet_over A);
defpred S₂[ Element of NAT ] means for p being FinSequence of A st len p = $1 holds
S₁[p];
A1: S₂[ 0 ]

proof

let p be FinSequence of A; :: thesis: ( len p = 0 implies S₁[p] )
assume len p = 0 ; :: thesis: S₁[p]
then p = <*> A ;
then |.p.| = A --> 0 by Th38
.= H₂( MultiSet_over A) by Th27
.= H₂( finite-MultiSet_over A) by MONOID_0:def 24 ;
hence S₁[p] ; :: thesis: verum

end;

A2: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A3: for p being FinSequence of A st len p = n holds
S₁[p] ; :: thesis: S₂[n + 1]
let p be FinSequence of A; :: thesis: ( len p = n + 1 implies S₁[p] )
assume A4: len p = n + 1 ; :: thesis: S₁[p]
then p <> {} ;
then consider r being FinSequence, x being set such that
A5: p = r ^ <*x*> by FINSEQ_1:63;
reconsider r = r as FinSequence of A by A5, FINSEQ_1:50;
len <*x*> = 1 by FINSEQ_1:57;
then A6: n + 1 = (len r) + 1 by A4, A5, FINSEQ_1:35;
rng <*x*> = {x} by FINSEQ_1:56;
then ( {x} c= rng p & rng p c= A ) by A5, FINSEQ_1:43;
then {x} c= A by XBOOLE_1:1;
then reconsider x = x as Element of A by ZFMISC_1:37;
set M = finite-MultiSet_over A;
reconsider r' = |.r.|, a = chi x as Element of (finite-MultiSet_over A) by A3, A6, Th34;
finite-MultiSet_over A is SubStr of MultiSet_over A by MONOID_0:23;
then r' [*] a = |.r.| [*] (chi x) by MONOID_0:27
.= |.p.| by A5, Th40 ;
hence S₁[p] ; :: thesis: verum

end;

A7: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A1, A2);
len p = len p ;
hence |.p.| is Element of (finite-MultiSet_over A) by A7; :: thesis: verum