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

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