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