let f be FinSequence of COMPLEX ; :: thesis: Sum (f | 1) = f . 1

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

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

then B2: 1 in dom f by FINSEQ_5:6;
f | 1 = <*(f /. 1)*> by B1, FINSEQ_5:20
.= <*(f . 1)*> by B2, PARTFUN1:def 6 ;
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 by RVSUM_2:29
.= f . 1 by B1 ;
hence Sum (f | 1) = f . 1 ; :: thesis: verum

end;

end;