per cases ( k > n or k <= n ) ;

suppose k > n ; :: thesis: (f,k) +...+ (f,n) is real

hence (f,k) +...+ (f,n) is real by Def1; :: thesis: verum

end;

suppose k <= n ; :: thesis: (f,k) +...+ (f,n) is real

then consider h being complex-valued FinSequence such that
A1: ( (f,k) +...+ (f,n) = Sum h & len h = (n -' k) + 1 ) and
A2: h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) by Th9;
rng h c= REAL

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in REAL )
assume y in rng h ; :: thesis: y in REAL
then consider x being object such that
A3: ( x in dom h & h . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
( 1 <= x & x <= len h ) by A3, FINSEQ_3:25;
then reconsider x1 = x - 1 as Nat ;
x1 + 1 <= (n -' k) + 1 by A3, FINSEQ_3:25, A1;
then x1 <= n -' k by XREAL_1:6;
then h . (x1 + 1) = f . (x1 + k) by A2;
hence y in REAL by A3, XREAL_0:def 1; :: thesis: verum

end;

then h is real-valued by VALUED_0:def 3;
hence (f,k) +...+ (f,n) is real by A1; :: thesis: verum

end;

end;