let f, F be FinSequence of REAL ; :: thesis: Sum (f ^ F) = (Sum f) + (Sum F)
( f is FinSequence of COMPLEX & F is FinSequence of COMPLEX ) by RVSUM_1:146;
hence Sum (f ^ F) = (Sum f) + (Sum F) by MATRIXC1:46; :: thesis: verum