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

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