let A be non empty set ; :: thesis: for p being FinSequence of A holds |.p.| is Element of
let p be FinSequence of A; :: thesis: |.p.| is Element of
defpred S1[ FinSequence of A] means |.\$1.| is Element of ;
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 ;
then A6: {x} c= A by XBOOLE_1:1;
reconsider r = r as FinSequence of A by ;
A7: len <*x*> = 1 by FINSEQ_1:40;
reconsider x = x as Element of A by ;
n + 1 = (len r) + 1 by ;
then reconsider r9 = |.r.|, a = chi x as Element of by ;
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 ;
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 by A1; :: thesis: verum