let F be FinSequence of ExtREAL ; :: thesis: for f being FinSequence of REAL st F = f holds
Sum F = Sum f
let f be FinSequence of REAL ; :: thesis: ( F = f implies Sum F = Sum f )
defpred S₁[ Nat] means for G being FinSequence of ExtREAL
for g being FinSequence of REAL st G = F | (Seg $1) & g = f | (Seg $1) & $1 <= len F holds
Sum G = Sum g;
F | (Seg (len F)) = F | (len F) by FINSEQ_1:def 16;
then A1: F | (Seg (len F)) = F by FINSEQ_1:58;
assume A2: F = f ; :: thesis: Sum F = Sum f
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
for G being FinSequence of ExtREAL
for g being FinSequence of REAL st G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F holds
Sum G = Sum g

proof

let G be FinSequence of ExtREAL ; :: thesis: for g being FinSequence of REAL st G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F holds
Sum G = Sum g
let g be FinSequence of REAL ; :: thesis: ( G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F implies Sum G = Sum g )
assume that
A5: G = F | (Seg (k + 1)) and
A6: g = f | (Seg (k + 1)) and
A7: k + 1 <= len F ; :: thesis: Sum G = Sum g
reconsider gk = g . (k + 1) as Element of REAL by XREAL_0:def 1;
reconsider g2 = <*gk*> as FinSequence of REAL ;
reconsider G1 = G | (Seg k) as FinSequence of ExtREAL by FINSEQ_1:18;
A8: ( not -infty in rng G1 & not -infty in rng <*(G . (k + 1))*> ) by A2, A5;
reconsider g1 = g | (Seg k) as FinSequence of REAL by FINSEQ_1:18;
len g = k + 1 by A2, A6, A7, FINSEQ_1:17;
then g = g1 ^ <*(g . (k + 1))*> by FINSEQ_3:55;
then A10: Sum g = (Sum g1) + (g . (k + 1)) by RVSUM_1:74;
A11: k <= k + 1 by NAT_1:11;
len G = k + 1 by A5, A7, FINSEQ_1:17;
then G = G1 ^ <*(G . (k + 1))*> by FINSEQ_3:55;
then A12: Sum G = (Sum G1) + (Sum <*(G . (k + 1))*>) by A8, EXTREAL1:10
.= (Sum G1) + (G . (k + 1)) by EXTREAL1:8 ;
k <= k + 1 by NAT_1:11;
then Seg k c= Seg (k + 1) by FINSEQ_1:5;
then ( G1 = F | (Seg k) & g1 = f | (Seg k) ) by A5, A6, FUNCT_1:51;
then Sum G1 = Sum g1 by A4, A7, A11, XXREAL_0:2;
hence Sum G = Sum g by A2, A5, A6, A12, A10, SUPINF_2:1; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A13: S₁[ 0 ] by EXTREAL1:7, RVSUM_1:72;
for k being Nat holds S₁[k] from NAT_1:sch 2(A13, A3);
hence Sum F = Sum f by A2, A1; :: thesis: verum