let f be complex-valued FinSequence; :: thesis: Sum (f | 1) = f . 1

per cases ( not f is empty or f is empty ) ;

suppose not f is empty ; :: thesis: Sum (f | 1) = f . 1

then f | 1 = <*(f . 1)*> by FINSEQ_5:20;
hence Sum (f | 1) = f . 1 ; :: thesis: verum

end;

suppose B1: f is empty ; :: thesis: Sum (f | 1) = f . 1

then Sum (f | 1) = 0
.= f . 1 by B1 ;
hence Sum (f | 1) = f . 1 ; :: thesis: verum

end;

end;