theorem :: FLEXARY1:48

for f being FinSequence of COMPLEX * holds Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f)