let f be INT -valued Real_Sequence; :: thesis: ( ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 implies Sum f is Integer )
given n being Nat such that A1: for k being Nat st k >= n holds
f . k = 0 ; :: thesis: Sum f is Integer
set p = Partial_Sums f;
reconsider pk = (Partial_Sums f) . n as Real ;
set r = seq_const pk;
for k being Nat st k >= n holds
(Partial_Sums f) . k = (seq_const pk) . k

proof

let k be Nat; :: thesis: ( k >= n implies (Partial_Sums f) . k = (seq_const pk) . k )
assume A2: k >= n ; :: thesis: (Partial_Sums f) . k = (seq_const pk) . k
defpred S₁[ Nat] means (Partial_Sums f) . $1 = (seq_const pk) . $1;
A3: S₁[n] by SEQ_1:57;
A4: for i being Nat st n <= i & S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( n <= i & S₁[i] implies S₁[i + 1] )
assume A5: n <= i ; :: thesis: ( not S₁[i] or S₁[i + 1] )
assume A6: S₁[i] ; :: thesis: S₁[i + 1]
(Partial_Sums f) . (i + 1) = ((Partial_Sums f) . i) + (f . (i + 1)) by SERIES_1:def 1
.= ((seq_const pk) . i) + 0 by A1, A5, A6, NAT_1:12
.= pk by SEQ_1:57
.= (seq_const pk) . (i + 1) ;
hence S₁[i + 1] ; :: thesis: verum

end;

for k being Nat st n <= k holds
S₁[k] from NAT_1:sch 8(A3, A4);
hence (Partial_Sums f) . k = (seq_const pk) . k by A2; :: thesis: verum

end;

then lim (Partial_Sums f) = lim (seq_const pk) by SEQ_4:19;
hence Sum f is Integer ; :: thesis: verum