let f be Real_Sequence; :: thesis: for n being Nat st f is summable & f . 0 = 0 holds

Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1)))

let n be Nat; :: thesis: ( f is summable & f . 0 = 0 implies Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1))) )

assume A1: ( f is summable & f . 0 = 0 ) ; :: thesis: Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1)))

then Sum f = ((Partial_Sums f) . n) + (Sum (f ^\ (n + 1))) by SERIES_1:15;

hence Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1))) by A1, Th21; :: thesis: verum

Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1)))

let n be Nat; :: thesis: ( f is summable & f . 0 = 0 implies Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1))) )

assume A1: ( f is summable & f . 0 = 0 ) ; :: thesis: Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1)))

then Sum f = ((Partial_Sums f) . n) + (Sum (f ^\ (n + 1))) by SERIES_1:15;

hence Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1))) by A1, Th21; :: thesis: verum