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 15;
then A1: F | (Seg (len F)) = F by FINSEQ_1:79;
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 g2 = <*(g . (k + 1))*> as FinSequence of REAL ;
reconsider G1 = G | (Seg k) as FinSequence of ExtREAL by FINSEQ_1:23;

A8: now

A9: rng g2 c= REAL ;
assume ( -infty in rng G1 or -infty in rng <*(G . (k + 1))*> ) ; :: thesis: contradiction
hence contradiction by A2, A5, A6, A9; :: thesis: verum

end;

reconsider g1 = g | (Seg k) as FinSequence of REAL by FINSEQ_1:23;
len g = k + 1 by A2, A6, A7, FINSEQ_1:21;
then g = g1 ^ <*(g . (k + 1))*> by FINSEQ_3:61;
then A10: Sum g = (Sum g1) + (g . (k + 1)) by RVSUM_1:104;
A11: k <= k + 1 by NAT_1:11;
len G = k + 1 by A5, A7, FINSEQ_1:21;
then G = G1 ^ <*(G . (k + 1))*> by FINSEQ_3:61;
then A12: Sum G = (Sum G1) + (Sum <*(G . (k + 1))*>) by A8, EXTREAL1:43
.= (Sum G1) + (G . (k + 1)) by EXTREAL1:41 ;
k <= k + 1 by NAT_1:11;
then Seg k c= Seg (k + 1) by FINSEQ_1:7;
then ( G1 = F | (Seg k) & g1 = f | (Seg k) ) by A5, A6, FUNCT_1:82;
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 ]

proof

let G be FinSequence of ExtREAL ; :: thesis: for g being FinSequence of REAL st G = F | (Seg 0 ) & g = f | (Seg 0 ) & 0 <= len F holds
Sum G = Sum g
let g be FinSequence of REAL ; :: thesis: ( G = F | (Seg 0 ) & g = f | (Seg 0 ) & 0 <= len F implies Sum G = Sum g )
assume Z: ( G = F | (Seg 0 ) & g = f | (Seg 0 ) ) ; :: thesis: ( not 0 <= len F or Sum G = Sum g )
assume 0 <= len F ; :: thesis: Sum G = Sum g
thus Sum G = 0 by EXTREAL1:40, Z
.= Sum g by RVSUM_1:102, Z ; :: thesis: verum

end;

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