let RFin be FinSequence of REAL ; :: 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;
thus Sum RFin = addreal $$ RFin by RVSUM_1:def 12
.= 0 by A1, A2, BINOP_2:2, FINSOP_1:def 1 ; :: thesis: verum