set g = Partial_Sums f;
rng (Partial_Sums f) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Partial_Sums f) or y in NAT )
assume y in rng (Partial_Sums f) ; :: thesis: y in NAT
then consider x being object such that
A0: ( x in dom (Partial_Sums f) & y = (Partial_Sums f) . x ) by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A0, FUNCT_2:def 1;
defpred S₁[ Nat] means (Partial_Sums f) . f is Nat;
(Partial_Sums f) . 0 = f . 0 by SERIES_1:def 1;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 12;
(Partial_Sums f) . (k + 1) = ((Partial_Sums f) . k) + (f . (k + 1)) by SERIES_1:def 1;
hence S₁[k + 1] by A3; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
then (Partial_Sums f) . n is Nat ;
hence y in NAT by A0, ORDINAL1:def 12; :: thesis: verum

end;

hence Partial_Sums f is NAT -valued by RELAT_1:def 19; :: thesis: verum