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_{1}[ FinSequence of A] means |.$1.| is Element of (finite-MultiSet_over A);

defpred S_{2}[ Nat] means for p being FinSequence of A st len p = $1 holds

S_{1}[p];

A1: len p = len p ;

A2: for n being Nat st S_{2}[n] holds

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

hence |.p.| is Element of (finite-MultiSet_over A) by A1; :: thesis: verum

let p be FinSequence of A; :: thesis: |.p.| is Element of (finite-MultiSet_over A)

defpred S

defpred S

S

A1: len p = len p ;

A2: for n being Nat st S

S

proof

A8:
S
set M = finite-MultiSet_over A;

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A3: for p being FinSequence of A st len p = n holds

S_{1}[p]
; :: thesis: S_{2}[n + 1]

let p be FinSequence of A; :: thesis: ( len p = n + 1 implies S_{1}[p] )

assume A4: len p = n + 1 ; :: thesis: S_{1}[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 S_{1}[p]
; :: thesis: verum

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

assume A3: for p being FinSequence of A st len p = n holds

S

let p be FinSequence of A; :: thesis: ( len p = n + 1 implies S

assume A4: len p = n + 1 ; :: thesis: S

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 S

proof

for n being Nat holds S
let p be FinSequence of A; :: thesis: ( len p = 0 implies S_{1}[p] )

assume len p = 0 ; :: thesis: S_{1}[p]

then p = <*> A ;

then |.p.| = A --> 0 by Th37

.= H_{2}( MultiSet_over A)
by Th26

.= H_{2}( finite-MultiSet_over A)
by MONOID_0:def 24
;

hence S_{1}[p]
; :: thesis: verum

end;assume len p = 0 ; :: thesis: S

then p = <*> A ;

then |.p.| = A --> 0 by Th37

.= H

.= H

hence S

hence |.p.| is Element of (finite-MultiSet_over A) by A1; :: thesis: verum