set g = Partial_Sums f;

rng (Partial_Sums f) c= NAT

rng (Partial_Sums f) c= NAT

proof

hence
Partial_Sums f is NAT -valued
by RELAT_1:def 19; :: thesis: verum
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_{1}[ Nat] means (Partial_Sums f) . f is Nat;

(Partial_Sums f) . 0 = f . 0 by SERIES_1:def 1;

then A1: S_{1}[ 0 ]
;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[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;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

(Partial_Sums f) . 0 = f . 0 by SERIES_1:def 1;

then A1: S

A2: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
by A3; :: thesis: verum

end;assume A3: S

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

then (Partial_Sums f) . n is Nat ;

hence y in NAT by A0, ORDINAL1:def 12; :: thesis: verum