let A be non empty set ; :: thesis: for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.|
let p, q be FinSequence of A; :: thesis: |.(p ^ q).| = |.p.| [*] |.q.|
defpred S₁[ Nat] means for q being FinSequence of A st len q = $1 holds
|.(p ^ q).| = |.p.| [*] |.q.|;
A1: len q = len q ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: for q being FinSequence of A st len q = n holds
|.(p ^ q).| = |.p.| [*] |.q.| ; :: thesis: S₁[n + 1]
let q be FinSequence of A; :: thesis: ( len q = n + 1 implies |.(p ^ q).| = |.p.| [*] |.q.| )
assume A4: len q = n + 1 ; :: thesis: |.(p ^ q).| = |.p.| [*] |.q.|
then q <> {} ;
then consider r being FinSequence, x being object such that
A5: q = r ^ <*x*> by FINSEQ_1:46;
rng <*x*> = {x} by FINSEQ_1:39;
then {x} c= rng q 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;
len <*x*> = 1 by FINSEQ_1:40;
then A7: n + 1 = (len r) + 1 by A4, A5, FINSEQ_1:22;
reconsider x = x as Element of A by A6, ZFMISC_1:31;
thus |.(p ^ q).| = |.((p ^ r) ^ <*x*>).| by A5, FINSEQ_1:32
.= |.(p ^ r).| [*] (chi x) by Th39
.= (|.p.| [*] |.r.|) [*] (chi x) by A3, A7
.= |.p.| [*] (|.r.| [*] (chi x)) by GROUP_1:def 3
.= |.p.| [*] |.q.| by A5, Th39 ; :: thesis: verum

end;

A8: S₁[ 0 ]

proof

let q be FinSequence of A; :: thesis: ( len q = 0 implies |.(p ^ q).| = |.p.| [*] |.q.| )
A9: ( |.(<*> A).| = A --> 0 & A --> 0 = H₂( MultiSet_over A) ) by Th26, Th37;
assume len q = 0 ; :: thesis: |.(p ^ q).| = |.p.| [*] |.q.|
then A10: q = {} ;
then p ^ q = p by FINSEQ_1:34;
hence |.(p ^ q).| = |.p.| [*] |.q.| by A10, A9, MONOID_0:16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A2);
hence |.(p ^ q).| = |.p.| [*] |.q.| by A1; :: thesis: verum