let f be V169() FinSequence of ExtREAL ; for s being V169() 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 V169() ExtREAL_sequence; ( ( 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
; (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 S1[ 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:
S1[ 0 ]
by A2, MESFUNC9:def 1;
a4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume a5:
S1[
k]
;
S1[k + 1]
hereby verum
assume a7:
k + 1
<= len f
;
( (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;
F . (k + 1) <> -infty thus
F . (k + 1) <> -infty
by d1, a5, a7, NAT_1:13, a8, XXREAL_3:17;
verum
end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(a3, a4);
hence
(Sum f) + (s . 0) = (Partial_Sums s) . (len f)
by A2; verum