let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL holds Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)

let F be Functional_Sequence of X,REAL; :: thesis: Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)

defpred S_{1}[ Nat] means (Partial_Sums (R_EAL F)) . $1 = (R_EAL (Partial_Sums F)) . $1;

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

S_{1}[k + 1]

.= R_EAL ((Partial_Sums F) . 0) by Def2 ;

then A2: S_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A2, A1);

hence Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F) ; :: thesis: verum

let F be Functional_Sequence of X,REAL; :: thesis: Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)

defpred S

A1: for k being Nat st S

S

proof

(Partial_Sums (R_EAL F)) . 0 =
(R_EAL F) . 0
by MESFUNC9:def 4
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then (Partial_Sums (R_EAL F)) . (k + 1) = (R_EAL ((Partial_Sums F) . k)) + (R_EAL (F . (k + 1))) by MESFUNC9:def 4

.= R_EAL (((Partial_Sums F) . k) + (F . (k + 1))) by MESFUNC6:23 ;

hence S_{1}[k + 1]
by Def2; :: thesis: verum

end;assume S

then (Partial_Sums (R_EAL F)) . (k + 1) = (R_EAL ((Partial_Sums F) . k)) + (R_EAL (F . (k + 1))) by MESFUNC9:def 4

.= R_EAL (((Partial_Sums F) . k) + (F . (k + 1))) by MESFUNC6:23 ;

hence S

.= R_EAL ((Partial_Sums F) . 0) by Def2 ;

then A2: S

for i being Nat holds S

hence Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F) ; :: thesis: verum