let f be complex-valued FinSequence; :: 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)

A0: f is FinSequence of COMPLEX by FINSEQ_1:107;
thus Sum ((f /^ n) | 1) = (f /^ n) . 1 by S1
.= f . (n + 1) by A1, A0, FINSEQ_7:4 ; :: 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;
thus Sum ((f /^ n) | 1) = 0 by A1
.= f . (n + 1) by A2, FUNCT_1:def 2 ; :: thesis: verum

end;

end;