let i be Nat; :: thesis: for f being complex-valued FinSequence holds Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1)))
let f be complex-valued FinSequence; :: thesis: Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1)))
set f1 = f | i;
set f2 = f /^ i;
set k = 1;
set f4 = (f /^ i) /^ 1;
Sum f = Sum ((f | i) ^ (f /^ i)) by RFINSEQ:8
.= (Sum (f | i)) + (Sum (f /^ i)) by RVSUM_2:32
.= (Sum (f | i)) + (Sum (((f /^ i) | 1) ^ ((f /^ i) /^ 1))) by RFINSEQ:8
.= (Sum (f | i)) + ((Sum ((f /^ i) | 1)) + (Sum ((f /^ i) /^ 1))) by RVSUM_2:32
.= (Sum (f | i)) + ((Sum ((f /^ i) | 1)) + (Sum (f /^ (i + 1)))) by FINSEQ681
.= ((Sum (f | i)) + (Sum ((f /^ i) | 1))) + (Sum (f /^ (i + 1))) ;
hence Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1))) by S2; :: thesis: verum