let F be FinSequence of COMPLEX ; :: thesis: ( len F = 1 implies Sum F = F . 1 )
assume len F = 1 ; :: thesis: Sum F = F . 1
then F = <*(F . 1)*> by FINSEQ_1:40;
hence Sum F = F . 1 by FINSOP_1:11; :: thesis: verum