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