let f be FinSequence of COMPLEX ; :: 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 by RVSUM_2:29
.= f . 1 by B1 ;
hence Sum (f | 1) = f . 1 ; :: thesis: verum
end;
end;