theorem Th45: :: FLEXARY1:45

for f being complex-valued FinSequence holds Sum <*f*> = <*(Sum f)*>