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

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