let seq be ExtREAL_sequence; :: thesis: Ser seq = Partial_Sums seq
for x being object st x in NAT holds
(Ser seq) . x = (Partial_Sums seq) . x

proof

defpred S₁[ Nat] means (Ser seq) . $1 = (Partial_Sums seq) . $1;
let x be object ; :: thesis: ( x in NAT implies (Ser seq) . x = (Partial_Sums seq) . x )
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 (Ser seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SUPINF_2:def 11;
hence S₁[k + 1] by MESFUNC9:def 1; :: thesis: verum

end;

assume x in NAT ; :: thesis: (Ser seq) . x = (Partial_Sums seq) . x
then reconsider n = x as Element of NAT ;
(Ser seq) . 0 = seq . 0 by SUPINF_2:def 11
.= (Partial_Sums seq) . 0 by MESFUNC9:def 1 ;
then A2: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
then (Ser seq) . x = (Partial_Sums seq) . n ;
hence (Ser seq) . x = (Partial_Sums seq) . x ; :: thesis: verum

end;

hence Ser seq = Partial_Sums seq by FUNCT_2:12; :: thesis: verum