theorem Th18: :: FLEXARY1:18

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