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

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

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

then 1 <= len f by NAT_1:14;
then B2: len (f | 1) = 1 by AFINSQ_1:54;
then 0 in Segm (len (f | 1)) by NAT_1:44;
then ( 0 in dom f & 0 in 1 ) by RELAT_1:57;
then B3: 0 in (dom f) /\ 1 by XBOOLE_0:def 4;
Sum (f | 1) = Sum <%((f | 1) . 0)%> by B2, AFINSQ_1:34
.= f . 0 by B3, FUNCT_1:48 ;
hence Sum (f | 1) = f . 0 ; :: thesis: verum

end;

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

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

end;

end;