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

for k being Nat st k >= n holds

f . k = 0 implies ex n being Nat st

for k being Nat st k >= n holds

(Partial_Sums f) . k = (Partial_Sums f) . n )

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

f . k = 0 ; :: thesis: ex n being Nat st

for k being Nat st k >= n holds

(Partial_Sums f) . k = (Partial_Sums f) . n

set p = Partial_Sums f;

reconsider pk = (Partial_Sums f) . n as Real ;

set r = seq_const pk;

A2: for k being Nat st k >= n holds

(Partial_Sums f) . k = (seq_const pk) . k

(Partial_Sums f) . k = (Partial_Sums f) . n

let k be Nat; :: thesis: ( k >= n implies (Partial_Sums f) . k = (Partial_Sums f) . n )

assume k >= n ; :: thesis: (Partial_Sums f) . k = (Partial_Sums f) . n

then (Partial_Sums f) . k = (seq_const pk) . k by A2

.= (Partial_Sums f) . n by SEQ_1:57 ;

hence (Partial_Sums f) . k = (Partial_Sums f) . n ; :: thesis: verum

for k being Nat st k >= n holds

f . k = 0 implies ex n being Nat st

for k being Nat st k >= n holds

(Partial_Sums f) . k = (Partial_Sums f) . n )

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

f . k = 0 ; :: thesis: ex n being Nat st

for k being Nat st k >= n holds

(Partial_Sums f) . k = (Partial_Sums f) . n

set p = Partial_Sums f;

reconsider pk = (Partial_Sums f) . n as Real ;

set r = seq_const pk;

A2: for k being Nat st k >= n holds

(Partial_Sums f) . k = (seq_const pk) . k

proof

take
n
; :: thesis: for k being Nat st k >= n holds
let k be Nat; :: thesis: ( k >= n implies (Partial_Sums f) . k = (seq_const pk) . k )

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

defpred S_{1}[ Nat] means (Partial_Sums f) . $1 = (seq_const pk) . $1;

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

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

S_{1}[i + 1]

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

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

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

defpred S

A4: S

A5: 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 A6: n <= i ; :: thesis: ( not S_{1}[i] or S_{1}[i + 1] )

assume A7: 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, A6, A7, NAT_1:12

.= pk by SEQ_1:57

.= (seq_const pk) . (i + 1) ;

hence S_{1}[i + 1]
; :: thesis: verum

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

assume A7: 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, A6, A7, 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 A3; :: thesis: verum

(Partial_Sums f) . k = (Partial_Sums f) . n

let k be Nat; :: thesis: ( k >= n implies (Partial_Sums f) . k = (Partial_Sums f) . n )

assume k >= n ; :: thesis: (Partial_Sums f) . k = (Partial_Sums f) . n

then (Partial_Sums f) . k = (seq_const pk) . k by A2

.= (Partial_Sums f) . n by SEQ_1:57 ;

hence (Partial_Sums f) . k = (Partial_Sums f) . n ; :: thesis: verum