let k, n be Nat; :: thesis: for f being complex-valued Function st (f,k) +...+ (f,n) <> 0 holds
ex i being Nat st
( k <= i & i <= n & i in dom f )
let f be complex-valued Function; :: thesis: ( (f,k) +...+ (f,n) <> 0 implies ex i being Nat st
( k <= i & i <= n & i in dom f ) )
assume A1: (f,k) +...+ (f,n) <> 0 ; :: thesis: ex i being Nat st
( k <= i & i <= n & i in dom f )
then A2: n >= k by Def1;
then consider h being complex-valued FinSequence such that
A3: (f,k) +...+ (f,n) = Sum h and
A4: len h = (n -' k) + 1 and
A5: h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) by Th9;
assume A6: for i being Nat st k <= i & i <= n holds
not i in dom f ; :: thesis: contradiction
(n -' k) + 1 >= 1 by NAT_1:11;
then 1 in dom h by A4, FINSEQ_3:25;
then A7: h . 1 in rng h by FUNCT_1:def 3;
rng h c= {0}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in {0} )
assume y in rng h ; :: thesis: y in {0}
then consider x being object such that
A8: ( x in dom h & h . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A8;
( 1 <= x & x <= len h ) by A8, FINSEQ_3:25;
then reconsider x1 = x - 1 as Nat ;
x1 + 1 = x ;
then A9: x1 <= n -' k by A8, FINSEQ_3:25, A4, XREAL_1:6;
then A10: h . (x1 + 1) = f . (x1 + k) by A5;
n -' k = n - k by A2, XREAL_1:233;
then ( k <= x1 + k & x1 + k <= (n -' k) + k & (n -' k) + k = n ) by A9, XREAL_1:6, NAT_1:11;
then not x1 + k in dom f by A6;
then f . (x1 + k) = 0 by FUNCT_1:def 2;
hence y in {0} by A10, A8, TARSKI:def 1; :: thesis: verum

end;

then h = (dom h) --> 0 by A7, ZFMISC_1:33, FUNCOP_1:9;
then h = (len h) |-> 0 by FINSEQ_1:def 3;
hence contradiction by RVSUM_1:81, A3, A1; :: thesis: verum