let F be without-infty FinSequence of ExtREAL ; :: thesis: for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
for i being Nat holds Sum (F | i) = (Partial_Sums G) . i
let G be ExtREAL_sequence; :: thesis: ( ( for i being Nat holds F . i = G . i ) implies for i being Nat holds Sum (F | i) = (Partial_Sums G) . i )
assume A1: for i being Nat holds F . i = G . i ; :: thesis: for i being Nat holds Sum (F | i) = (Partial_Sums G) . i

hereby :: thesis: verum

let i be Nat; :: thesis: Sum (F | i) = (Partial_Sums G) . i
defpred S₁[ Nat] means Sum (F | $1) = (Partial_Sums G) . $1;
A3: ex f0 being sequence of ExtREAL st
( Sum (F | 0) = f0 . (len (F | 0)) & f0 . 0 = 0. & ( for i being Nat st i < len (F | 0) holds
f0 . (i + 1) = (f0 . i) + ((F | 0) . (i + 1)) ) ) by EXTREAL1:def 2;
not 0 in Seg (len F) by FINSEQ_1:1;
then not 0 in dom F by FINSEQ_1:def 3;
then F . 0 = 0 by FUNCT_1:def 2;
then G . 0 = 0 by A1;
then A4: S₁[ 0 ] by A3, MESFUNC9:def 1;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
F | k is without-infty by Th34;
then A7: not -infty in rng (F | k) by MESFUNC5:def 3;

A8: now :: thesis: not -infty in rng <*(F . (k + 1))*>

assume -infty in rng <*(F . (k + 1))*> ; :: thesis: contradiction
then -infty in {(F . (k + 1))} by FINSEQ_1:39;
then A9: F . (k + 1) = -infty by TARSKI:def 1;

per cases ( k + 1 in dom F or not k + 1 in dom F ) ;

suppose k + 1 in dom F ; :: thesis: contradiction

then F . (k + 1) in rng F by FUNCT_1:3;
hence contradiction by A9, MESFUNC5:def 3; :: thesis: verum

end;

suppose not k + 1 in dom F ; :: thesis: contradiction

hence contradiction by A9, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

per cases ( k + 1 <= len F or k + 1 > len F ) ;

suppose k + 1 <= len F ; :: thesis: S₁[k + 1]

then F | (k + 1) = (F | k) ^ <*(F . (k + 1))*> by NAT_1:13, FINSEQ_5:83;
then Sum (F | (k + 1)) = (Sum (F | k)) + (Sum <*(F . (k + 1))*>) by A7, A8, EXTREAL1:10
.= ((Partial_Sums G) . k) + (F . (k + 1)) by A6, Th33
.= ((Partial_Sums G) . k) + (G . (k + 1)) by A1 ;
hence S₁[k + 1] by MESFUNC9:def 1; :: thesis: verum

end;

suppose A10: k + 1 > len F ; :: thesis: S₁[k + 1]

then A11: ( F | k = F & F | (k + 1) = F ) by NAT_1:13, FINSEQ_1:58;
not k + 1 in dom F by A10, FINSEQ_3:25;
then F . (k + 1) = 0 by FUNCT_1:def 2;
then G . (k + 1) = 0 by A1;
then (Partial_Sums G) . (k + 1) = ((Partial_Sums G) . k) + 0 by MESFUNC9:def 1;
hence S₁[k + 1] by A6, A11, XXREAL_3:4; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
hence Sum (F | i) = (Partial_Sums G) . i ; :: thesis: verum

end;