theorem Th22: :: FLEXARY1:22

for h being complex-valued FinSequence holds Sum h = (h . 1) + ((h,2) +...)