let RFin be real-valued FinSequence; :: thesis: ( len RFin = 0 implies Sum RFin = 0 )
assume A1: len RFin = 0 ; :: thesis: Sum RFin = 0
0 in REAL by XREAL_0:def 1;
then A2: addreal is having_a_unity by RVSUM_1:1, SETWISEO:def 2;
reconsider RFin = RFin as FinSequence of REAL by FINSEQ_1:106;
Sum RFin = addreal $$ RFin by RVSUM_1:def 12
.= 0 by A1, A2, BINOP_2:2, FINSOP_1:def 1 ;
hence Sum RFin = 0 ; :: thesis: verum