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
( G is summable & Sum F = Sum G )
let G be ExtREAL_sequence; :: thesis: ( ( for i being Nat holds F . i = G . i ) implies ( G is summable & Sum F = Sum G ) )
assume A1: for i being Nat holds F . i = G . i ; :: thesis: ( G is summable & Sum F = Sum G )
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]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
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: verum

end;

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

hereby :: thesis: verum

per cases ( Sum F in REAL or Sum F = +infty or Sum F = -infty ) by XXREAL_0:14;

suppose Sum F in REAL ; :: thesis: ( G is summable & Sum F = Sum G )

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

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums G) . m) - r).| < p )
assume A6: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums G) . m) - r).| < p
take n = len F; :: thesis: for m being Nat st n <= m holds
|.(((Partial_Sums G) . m) - r).| < p

now :: thesis: for m being Nat st len F <= m holds
|.(((Partial_Sums G) . m) - r).| < p

let m be Nat; :: thesis: ( len F <= m implies |.(((Partial_Sums G) . m) - r).| < p )
assume len F <= m ; :: thesis: |.(((Partial_Sums G) . m) - r).| < p
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: verum

end;

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

end;

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

end;

suppose A7: Sum F = +infty ; :: thesis: ( G is summable & Sum F = Sum G )

now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= (Partial_Sums G) . m

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

proof

take n = len F; :: thesis: for m being Nat st n <= m holds
g <= (Partial_Sums G) . m

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies g <= (Partial_Sums G) . m )
assume n <= m ; :: thesis: g <= (Partial_Sums G) . m
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: verum

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: Sum F = Sum G
lim (Partial_Sums G) = Sum F by A7, B5, MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3; :: thesis: verum

end;

suppose A8: Sum F = -infty ; :: thesis: ( G is summable & Sum F = Sum G )

now :: thesis: for g being Real st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(Partial_Sums G) . m <= g

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

proof

take n = len F; :: thesis: for m being Nat st n <= m holds
(Partial_Sums G) . m <= g

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies (Partial_Sums G) . m <= g )
assume n <= m ; :: thesis: (Partial_Sums G) . m <= g
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: verum

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: Sum F = Sum G
lim (Partial_Sums G) = Sum F by A8, B8, MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3; :: thesis: verum

end;

end;

end;