let f be Real_Sequence; :: thesis: ( ex n being Nat st

for k being Nat st k >= n holds

f . k = 0 implies f is summable )

given n being Nat such that A1: for k being Nat st k >= n holds

f . k = 0 ; :: thesis: f is summable

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

for k being Nat st k >= n holds

f . k = 0 implies f is summable )

given n being Nat such that A1: for k being Nat st k >= n holds

f . k = 0 ; :: thesis: f is summable

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

hence
f is summable
by SEQ_4:18; :: thesis: verum
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_{1}[ Nat] means (Partial_Sums f) . $1 = (seq_const pk) . $1;

A3: S_{1}[n]
by SEQ_1:57;

A4: for i being Nat st n <= i & S_{1}[i] holds

S_{1}[i + 1]

S_{1}[k]
from NAT_1:sch 8(A3, A4);

hence (Partial_Sums f) . k = (seq_const pk) . k by A2; :: thesis: verum

end;assume A2: k >= n ; :: thesis: (Partial_Sums f) . k = (seq_const pk) . k

defpred S

A3: S

A4: for i being Nat st n <= i & S

S

proof

for k being Nat st n <= k holds
let i be Nat; :: thesis: ( n <= i & S_{1}[i] implies S_{1}[i + 1] )

assume A5: n <= i ; :: thesis: ( not S_{1}[i] or S_{1}[i + 1] )

assume A6: S_{1}[i]
; :: thesis: S_{1}[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_{1}[i + 1]
; :: thesis: verum

end;assume A5: n <= i ; :: thesis: ( not S

assume A6: S

(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

S

hence (Partial_Sums f) . k = (seq_const pk) . k by A2; :: thesis: verum