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_{1}[ 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_{1}[n] holds

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

hence |.(p ^ q).| = |.p.| [*] |.q.| by A1; :: thesis: verum

let p, q be FinSequence of A; :: thesis: |.(p ^ q).| = |.p.| [*] |.q.|

defpred S

|.(p ^ q).| = |.p.| [*] |.q.|;

A1: len q = len q ;

A2: for n being Nat st S

S

proof

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

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

|.(p ^ q).| = |.p.| [*] |.q.| ; :: thesis: S_{1}[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;assume A3: for q being FinSequence of A st len q = n holds

|.(p ^ q).| = |.p.| [*] |.q.| ; :: thesis: S

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

proof

for n being Nat holds S
let q be FinSequence of A; :: thesis: ( len q = 0 implies |.(p ^ q).| = |.p.| [*] |.q.| )

A9: ( |.(<*> A).| = A --> 0 & A --> 0 = H_{2}( 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;A9: ( |.(<*> A).| = A --> 0 & A --> 0 = H

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

hence |.(p ^ q).| = |.p.| [*] |.q.| by A1; :: thesis: verum