let f be INT -valued Real_Sequence; :: thesis: for n being Nat st f . 0 = 0 holds

Sum (f |_ (Seg n)) is Integer

let n be Nat; :: thesis: ( f . 0 = 0 implies Sum (f |_ (Seg n)) is Integer )

assume A1: f . 0 = 0 ; :: thesis: Sum (f |_ (Seg n)) is Integer

set ff = f |_ (Seg n);

Sum (f |_ (Seg n)) = (Partial_Sums f) . n by Th22, A1;

hence Sum (f |_ (Seg n)) is Integer ; :: thesis: verum

Sum (f |_ (Seg n)) is Integer

let n be Nat; :: thesis: ( f . 0 = 0 implies Sum (f |_ (Seg n)) is Integer )

assume A1: f . 0 = 0 ; :: thesis: Sum (f |_ (Seg n)) is Integer

set ff = f |_ (Seg n);

Sum (f |_ (Seg n)) = (Partial_Sums f) . n by Th22, A1;

hence Sum (f |_ (Seg n)) is Integer ; :: thesis: verum