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:110;
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: now

let j be Nat; :: thesis: ( j in Seg (len F) implies ((len F) |-> 0 ) . j = R2 . j )
assume A4: j in Seg (len F) ; :: thesis: ((len F) |-> 0 ) . j = R2 . j
then ((len F) |-> 0 ) . j = 0 by FUNCOP_1:13;
hence ((len F) |-> 0 ) . j = R2 . j by A2, A1, A4; :: thesis: verum

end;

len ((len F) |-> 0 ) = len F by FINSEQ_1:def 18;
then dom ((len F) |-> 0 ) = dom R2 by FINSEQ_3:31;
then (len F) |-> 0 = R2 by A1, A3, FINSEQ_1:17;
hence Sum F = 0 by RVSUM_1:111; :: thesis: verum