theorem Th21: :: MATRIXC1:23
for F being FinSequence of COMPLEX st len F >= 1 holds
Sum (F *') = (Sum F) *'