theorem Th45: :: FLEXARY1:45
for f being complex-valued FinSequence holds Sum <*f*> = <*(Sum f)*>