set f = Partial_Sums s;

let x be object ; :: according to VALUED_0:def 9 :: thesis: ( not x in dom (Partial_Sums s) or (Partial_Sums s) . x is real )

assume x in dom (Partial_Sums s) ; :: thesis: (Partial_Sums s) . x is real

then reconsider n = x as Element of NAT ;

defpred S_{1}[ Nat] means (Partial_Sums s) . s is real ;

(Partial_Sums s) . 0 = s . 0 by Def1;

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 s) . n is real ;

hence (Partial_Sums s) . x is real ; :: thesis: verum

let x be object ; :: according to VALUED_0:def 9 :: thesis: ( not x in dom (Partial_Sums s) or (Partial_Sums s) . x is real )

assume x in dom (Partial_Sums s) ; :: thesis: (Partial_Sums s) . x is real

then reconsider n = x as Element of NAT ;

defpred S

(Partial_Sums s) . 0 = s . 0 by Def1;

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 s) . (k + 1) = ((Partial_Sums s) . k) + (s . (k + 1)) by Def1;

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 s) . (k + 1) = ((Partial_Sums s) . k) + (s . (k + 1)) by Def1;

hence S

then (Partial_Sums s) . n is real ;

hence (Partial_Sums s) . x is real ; :: thesis: verum