theorem Th21: :: FLEXARY1:21

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