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₁[ Nat] means (Partial_Sums (R_EAL F)) . $1 = (R_EAL (Partial_Sums F)) . $1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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₁[k + 1] by Def2; :: thesis: verum

end;

(Partial_Sums (R_EAL F)) . 0 = (R_EAL F) . 0 by MESFUNC9:def 4
.= R_EAL ((Partial_Sums F) . 0) by Def2 ;
then A2: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A1);
hence Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F) ; :: thesis: verum