set CC = COMPLEX -concatenation ;
defpred S₁[ Nat] means for f being FinSequence of COMPLEX * st len f = $1 holds
Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f);
A1: ( COMPLEX -concatenation is having_a_unity & the_unity_wrt (COMPLEX -concatenation) = {} ) by MONOID_0:67;
A2: S₁[ 0 ]

proof

let f be FinSequence of COMPLEX * ; :: thesis: ( len f = 0 implies Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f) )
assume A3: len f = 0 ; :: thesis: Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f)
then Sum f = {} ;
hence Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f) by A1, A3, FINSOP_1:def 1; :: thesis: verum

end;

A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
let f be FinSequence of COMPLEX * ; :: thesis: ( len f = i + 1 implies Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f) )
assume A6: len f = i + 1 ; :: thesis: Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f)
then consider q being FinSequence of COMPLEX * , d being Element of COMPLEX * such that
A7: f = q ^ <*d*> by FINSEQ_2:19;
(len q) + 1 = len f by A7, FINSEQ_2:16;
then A8: Sum (Sum q) = Sum ((COMPLEX -concatenation) "**" q) by A6, A5;
Sum f = (Sum q) ^ (Sum <*d*>) by A7, Th46
.= (Sum q) ^ <*(Sum d)*> by Th45 ;
then A9: Sum (Sum f) = (Sum (Sum q)) + (Sum d) by RVSUM_2:31;
(COMPLEX -concatenation) "**" f = ((COMPLEX -concatenation) "**" q) ^ ((COMPLEX -concatenation) "**" <*d*>) by Th3, A7
.= ((COMPLEX -concatenation) "**" q) ^ d by FINSOP_1:11 ;
hence Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f) by RVSUM_2:32, A8, A9; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A4);
hence for f being FinSequence of COMPLEX * holds Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f) ; :: thesis: verum