let f be without-infty FinSequence of ExtREAL ; :: thesis: for s being without-infty ExtREAL_sequence st ( for n being object st n in dom f holds
f . n = s . n ) holds
(Sum f) + (s . 0) = (Partial_Sums s) . (len f)
let s be without-infty ExtREAL_sequence; :: thesis: ( ( for n being object st n in dom f holds
f . n = s . n ) implies (Sum f) + (s . 0) = (Partial_Sums s) . (len f) )
assume A1: for n being object st n in dom f holds
f . n = s . n ; :: thesis: (Sum f) + (s . 0) = (Partial_Sums s) . (len f)
consider F being sequence of ExtREAL such that
A2: ( Sum f = F . (len f) & F . 0 = 0 & ( for i being Nat st i < len f holds
F . (i + 1) = (F . i) + (f . (i + 1)) ) ) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len f implies ( (F . $1) + (s . 0) = (Partial_Sums s) . $1 & F . $1 <> -infty ) );
(F . 0) + (s . 0) = s . 0 by A2, XXREAL_3:4;
then a3: S₁[ 0 ] by A2, MESFUNC9:def 1;
a4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume a5: S₁[k] ; :: thesis: S₁[k + 1]

hereby :: thesis: verum

assume a7: k + 1 <= len f ; :: thesis: ( (F . (k + 1)) + (s . 0) = (Partial_Sums s) . (k + 1) & F . (k + 1) <> -infty )
then b0: k + 1 in dom f by NAT_1:11, FINSEQ_3:25;
then a8: f . (k + 1) <> -infty by MESFUNC5:10;
dom s = NAT by FUNCT_2:def 1;
then a9: s . 0 <> -infty by MESFUNC5:10;
d1: F . (k + 1) = (F . k) + (f . (k + 1)) by A2, a7, NAT_1:13;
then (F . (k + 1)) + (s . 0) = ((F . k) + (s . 0)) + (f . (k + 1)) by a5, a7, NAT_1:13, a8, a9, XXREAL_3:29
.= ((Partial_Sums s) . k) + (s . (k + 1)) by b0, A1, a5, a7, NAT_1:13 ;
hence (F . (k + 1)) + (s . 0) = (Partial_Sums s) . (k + 1) by MESFUNC9:def 1; :: thesis: F . (k + 1) <> -infty
thus F . (k + 1) <> -infty by d1, a5, a7, NAT_1:13, a8, XXREAL_3:17; :: thesis: verum

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(a3, a4);
hence (Sum f) + (s . 0) = (Partial_Sums s) . (len f) by A2; :: thesis: verum