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