let seq be Function of NAT,REAL; :: thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq holds
Partial_Sums seq = Ser Eseq
let Eseq be Function of NAT,ExtREAL; :: thesis: ( seq = Eseq implies Partial_Sums seq = Ser Eseq )
assume A1: seq = Eseq ; :: thesis: Partial_Sums seq = Ser Eseq
reconsider Ps = Partial_Sums seq as Function of NAT,ExtREAL by FUNCT_2:9, NUMBERS:31;
defpred S₁[ Element of NAT ] means Ps . $1 = (Ser Eseq) . $1;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: Ps . k = (Ser Eseq) . k ; :: thesis: S₁[k + 1]
Ps . k = (Partial_Sums seq) . k ;
then reconsider Psk = Ps . k as Real ;
( Ps . (k + 1) = Psk + (seq . (k + 1)) & (Ser Eseq) . (k + 1) = ((Ser Eseq) . k) + (Eseq . (k + 1)) ) by SERIES_1:def 1, SUPINF_2:63;
hence S₁[k + 1] by A1, A3, SUPINF_2:1; :: thesis: verum

end;

Ps . 0 = Eseq . 0 by A1, SERIES_1:def 1
.= (Ser Eseq) . 0 by SUPINF_2:63 ;
then A4: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A2);
hence Partial_Sums seq = Ser Eseq by FUNCT_2:113; :: thesis: verum