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 )
assume A1: F = f ; :: thesis: 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;
A2: S₁[ 0 ] by CONVFUN1:4, RVSUM_1:102;
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]
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 A6: ( G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F ) ; :: thesis: Sum G = Sum g
then A7: ( len G = k + 1 & dom G = Seg (k + 1) ) by FINSEQ_1:21;
reconsider G1 = G | (Seg k) as FinSequence of ExtREAL by FINSEQ_1:23;
A8: G = G1 ^ <*(G . (k + 1))*> by A7, FINSEQ_3:61;
A9: ( len g = k + 1 & dom g = Seg (k + 1) ) by A1, A6, FINSEQ_1:21;
reconsider g1 = g | (Seg k) as FinSequence of REAL by FINSEQ_1:23;
A10: g = g1 ^ <*(g . (k + 1))*> by A9, FINSEQ_3:61;
reconsider g2 = <*(g . (k + 1))*> as FinSequence of REAL ;
k <= k + 1 by NAT_1:11;
then Seg k c= Seg (k + 1) by FINSEQ_1:7;
then A11: ( G1 = F | (Seg k) & g1 = f | (Seg k) ) by A6, FUNCT_1:82;
k <= k + 1 by NAT_1:11;
then A12: Sum G1 = Sum g1 by A5, A6, A11, XXREAL_0:2;
( not -infty in rng G1 & not -infty in rng <*(G . (k + 1))*> )

proof

now

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

end;

hence ( not -infty in rng G1 & not -infty in rng <*(G . (k + 1))*> ) ; :: thesis: verum

end;

then A14: Sum G = (Sum G1) + (Sum <*(G . (k + 1))*>) by A8, CONVFUN1:7
.= (Sum G1) + (G . (k + 1)) by CONVFUN1:5 ;
Sum g = (Sum g1) + (g . (k + 1)) by A10, RVSUM_1:104;
hence Sum G = Sum g by A1, A6, A12, A14, SUPINF_2:1; :: thesis: verum

end;

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

end;

A15: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A4);
( F | (Seg (len F)) = F | (len F) & f | (len f) = f | (Seg (len f)) ) by FINSEQ_1:def 15;
then ( F | (Seg (len F)) = F & f | (Seg (len f)) = f ) by FINSEQ_1:79;
hence Sum F = Sum f by A1, A15; :: thesis: verum