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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: for q being FinSequence of A st len q = n holds
|.(p ^ q).| = |.p.| [*] |.q.| ; :: thesis: S1[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 ;
then A6: {x} c= A by XBOOLE_1:1;
reconsider r = r as FinSequence of A by ;
len <*x*> = 1 by FINSEQ_1:40;
then A7: n + 1 = (len r) + 1 by ;
reconsider x = x as Element of A by ;
thus |.(p ^ q).| = |.((p ^ r) ^ <*x*>).| by
.= |.(p ^ r).| [*] (chi x) by Th39
.= () [*] (chi x) by A3, A7
.= |.p.| [*] (|.r.| [*] (chi x)) by GROUP_1:def 3
.= |.p.| [*] |.q.| by ; :: thesis: verum
end;
A8: S1[ 0 ]
proof
let q be FinSequence of A; :: thesis: ( len q = 0 implies |.(p ^ q).| = |.p.| [*] |.q.| )
A9: ( |.(<*> A).| = A --> 0 & A --> 0 = H2( MultiSet_over A) ) by ;
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 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A8, A2);
hence |.(p ^ q).| = |.p.| [*] |.q.| by A1; :: thesis: verum