let f be complex-valued FinSequence; :: thesis: Sum f = (f . 1) + (Sum (f /^ 1))
reconsider f = f as FinSequence of COMPLEX by RVSUM_1:146;
Sum f = Sum ((f | 1) ^ (f /^ 1))
.= (Sum (f | 1)) + (Sum (f /^ 1)) by RVSUM_2:32 ;
hence Sum f = (f . 1) + (Sum (f /^ 1)) by NEWTON04:33; :: thesis: verum