let rF be real-valued XFinSequence; :: thesis: ( rF is nonnegative-yielding implies ( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) ) )
assume A1: rF is nonnegative-yielding ; :: thesis: ( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) )
hereby :: thesis: ( ( len rF = 0 or rF = (len rF) --> 0 ) implies Sum rF = 0 )
assume A2: Sum rF = 0 ; :: thesis: ( len rF <> 0 implies not rF <> (len rF) --> 0 )
assume A3: len rF <> 0 ; :: thesis: not rF <> (len rF) --> 0
set L = (len rF) --> 0;
assume rF <> (len rF) --> 0 ; :: thesis: contradiction
then consider k being Nat such that
A4: ( k in dom ((len rF) --> 0) & ((len rF) --> 0) . k <> rF . k ) by AFINSQ_1:8, FUNCOP_1:13;
rF . k in rng rF by A4, FUNCT_1:def 3;
then ( ((len rF) --> 0) . k = 0 & rF . k >= 0 ) by A4, A1, FUNCOP_1:7, PARTFUN3:def 4;
hence contradiction by A2, Th60, A1, A4, A3; :: thesis: verum
end;
A5: rF is COMPLEX -valued by Lm2;
assume ( len rF = 0 or rF = (len rF) --> 0 ) ; :: thesis: Sum rF = 0
then ( Sum rF = 0 or Sum rF = (len rF) * 0 ) by A5, Th57, Def8, BINOP_2:1;
hence Sum rF = 0 ; :: thesis: verum