let F be FinSequence of REAL ; :: thesis: ( ( for i being Element of NAT st i in dom F holds
F . i = 0 ) implies Sum F = 0 )
set i = len F;
set R1 = (len F) |-> 0;
reconsider R2 = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: Seg (len F) = dom F by FINSEQ_1:def 3;
assume A2: for i being Element of NAT st i in dom F holds
0 = F . i ; :: thesis: Sum F = 0
A3: for j being Nat st j in Seg (len F) holds
((len F) |-> 0) . j = R2 . j by A2, A1;
len ((len F) |-> 0) = len F by CARD_1:def 7;
then dom ((len F) |-> 0) = dom R2 by FINSEQ_3:29;
then (len F) |-> 0 = R2 by A1, A3, FINSEQ_1:13;
hence Sum F = 0 by RVSUM_1:81; :: thesis: verum