theorem Th2: :: HILB10_1:2

for f being complex-valued FinSequence ex e, o being complex-valued FinSequence st
( len e = [\((len f) / 2)/] & len o = [/((len f) / 2)\] & Sum f = (Sum e) + (Sum o) & ( for n being Nat holds
( e . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) )