let f be Real_Sequence; :: thesis: for n being Nat st f . 0 = 0 holds
Sum (f |_ (Seg n)) = (Partial_Sums f) . n
let n be Nat; :: thesis: ( f . 0 = 0 implies Sum (f |_ (Seg n)) = (Partial_Sums f) . n )
assume A1: f . 0 = 0 ; :: thesis: Sum (f |_ (Seg n)) = (Partial_Sums f) . n
Sum (FinSeq (f,n)) = (Partial_Sums f) . n by A1, Th21;
hence Sum (f |_ (Seg n)) = (Partial_Sums f) . n by A1, Th18; :: thesis: verum