let f be FinSequence of COMPLEX ; :: thesis: for n being Nat holds Sum ((f /^ n) | 1) = f . (n + 1)
let n be Nat; :: thesis: Sum ((f /^ n) | 1) = f . (n + 1)

per cases ( 1 in dom (f /^ n) or not 1 in dom (f /^ n) ) ;

suppose A1: 1 in dom (f /^ n) ; :: thesis: Sum ((f /^ n) | 1) = f . (n + 1)

Sum ((f /^ n) | 1) = (f /^ n) . 1 by S1
.= f . (n + 1) by A1, FINSEQ_7:4 ;
hence Sum ((f /^ n) | 1) = f . (n + 1) ; :: thesis: verum

end;

suppose not 1 in dom (f /^ n) ; :: thesis: Sum ((f /^ n) | 1) = f . (n + 1)

then A1: f /^ n is empty by FINSEQ_5:6;
then 0 = len (f /^ n)
.= (len f) -' n by RFINSEQ:29 ;
then ( len f = n or 0 + n >= ((len f) - n) + n ) by XREAL_0:def 2, XREAL_1:6;
then (len f) + 0 < n + 1 by XREAL_1:8;
then A2: not n + 1 in dom f by FINSEQ_3:25;
Sum ((f /^ n) | 1) = 0 by A1, RVSUM_2:29
.= f . (n + 1) by A2, FUNCT_1:def 2 ;
hence Sum ((f /^ n) | 1) = f . (n + 1) ; :: thesis: verum

end;

end;