let RFin be FinSequence of REAL ; :: thesis: ( len RFin = 0 implies Sum RFin = 0 )
assume A1: len RFin = 0 ; :: thesis: Sum RFin = 0
A2: addreal is having_a_unity by RVSUM_1:3, SETWISEO:def 2;
thus Sum RFin = addreal $$ RFin by RVSUM_1:def 13
.= 0 by A1, A2, BINOP_2:2, FINSOP_1:def 1 ; :: thesis: verum