let F be V251() FinSequence of ExtREAL ; :: thesis:
let G be ExtREAL_sequence; :: thesis:
assume A1: for i being Nat holds F . i = G . i ; :: thesis:
then A2: Sum (F | (len F)) = (Partial_Sums G) . (len F) by Th35;
defpred S₁[ Nat] means Sum F = (Partial_Sums G) . ((len F) + $1);
B1: S₁[ 0 ] by A2, FINSEQ_1:58;
B2: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
len F < (len F) + (k + 1) by NAT_1:11, NAT_1:19;
then not ((len F) + k) + 1 in dom F by FINSEQ_3:25;
then F . (((len F) + k) + 1) = 0 by FUNCT_1:def 2;
then A4: G . (((len F) + k) + 1) = 0 by A1;
(Partial_Sums G) . ((len F) + (k + 1)) = ((Partial_Sums G) . ((len F) + k)) + (G . (((len F) + k) + 1)) by MESFUNC9:def 1
.= (Partial_Sums G) . ((len F) + k) by A4, XXREAL_3:4 ;
hence S₁[k + 1] by A3; :: thesis:

end;

A5: for k being Nat holds S₁[k] from NAT_1:sch 2(B1, B2);

hereby :: thesis:

per cases by XXREAL_0:14;

suppose Sum F in REAL ; :: thesis:

then reconsider r = Sum F as Real ;
B1: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums G) . m) - r).| < p

let p be Real; :: thesis:
assume A6: 0 < p ; :: thesis:
take n = len F; :: thesis:

let m be Nat; :: thesis:
assume len F <= m ; :: thesis:
then reconsider k = m - n as Nat by NAT_1:21;
m = n + k ;
then (Partial_Sums G) . m = Sum F by A5;
hence |.(((Partial_Sums G) . m) - r).| < p by A6, XXREAL_3:7, EXTREAL1:16; :: thesis:

end;

hence for m being Nat st n <= m holds
|.(((Partial_Sums G) . m) - r).| < p ; :: thesis:

end;

then B2: Partial_Sums G is convergent_to_finite_number by MESFUNC5:def 8;
hence G is summable by MESFUNC9:def 2; :: thesis:
lim (Partial_Sums G) = Sum F by B1, B2, MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3; :: thesis:

end;

suppose A7: Sum F = +infty ; :: thesis:

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
thus ex n being Nat st
for m being Nat st n <= m holds
g <= (Partial_Sums G) . m :: thesis:

take n = len F; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then reconsider k = m - n as Nat by NAT_1:21;
m = n + k ;
then (Partial_Sums G) . m = +infty by A5, A7;
hence g <= (Partial_Sums G) . m by XXREAL_0:3; :: thesis:

end;

end;

end;

then B5: Partial_Sums G is convergent_to_+infty by MESFUNC5:def 9;
hence G is summable by MESFUNC9:def 2; :: thesis:
lim (Partial_Sums G) = Sum F by A7, B5, MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3; :: thesis:

end;

suppose A8: Sum F = -infty ; :: thesis:

let g be Real; :: thesis:
assume g < 0 ; :: thesis:
thus ex n being Nat st
for m being Nat st n <= m holds
(Partial_Sums G) . m <= g :: thesis:

take n = len F; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then reconsider k = m - n as Nat by NAT_1:21;
m = n + k ;
then (Partial_Sums G) . m = -infty by A5, A8;
hence (Partial_Sums G) . m <= g by XXREAL_0:5; :: thesis:

end;

end;

end;

then B8: Partial_Sums G is convergent_to_-infty by MESFUNC5:def 10;
hence G is summable by MESFUNC9:def 2; :: thesis:
lim (Partial_Sums G) = Sum F by A8, B8, MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3; :: thesis:

end;

end;

end;