let f be nonnegative FinSequence of ExtREAL ; :: thesis: for s being ExtREAL_sequence st ( for n being object st n in dom f holds
f . n = s . n ) & ( for n being Element of NAT st not n in dom f holds
s . n = 0 ) holds
( Sum f = Sum s & Sum f = SUM s )
let s be ExtREAL_sequence; :: thesis: ( ( for n being object st n in dom f holds
f . n = s . n ) & ( for n being Element of NAT st not n in dom f holds
s . n = 0 ) implies ( Sum f = Sum s & Sum f = SUM s ) )
assume that
a1: for n being object st n in dom f holds
f . n = s . n and
a2: for n being Element of NAT st not n in dom f holds
s . n = 0 ; :: thesis: ( Sum f = Sum s & Sum f = SUM s )
for n being object st n in dom s holds
0 <= s . n

proof

let n be object ; :: thesis: ( n in dom s implies 0 <= s . n )
assume L1: n in dom s ; :: thesis: 0 <= s . n

per cases ( n in dom f or not n in dom f ) ;

suppose n in dom f ; :: thesis: 0 <= s . n

then f . n = s . n by a1;
hence 0 <= s . n by SUPINF_2:51; :: thesis: verum

end;

suppose not n in dom f ; :: thesis: 0 <= s . n

hence 0 <= s . n by a2, L1; :: thesis: verum

end;

end;

end;

then a7: s is nonnegative by SUPINF_2:52;
then a5: (Sum f) + (s . 0) = (Partial_Sums s) . (len f) by a1, Th36;
not 0 in dom f by FINSEQ_3:24;
then s . 0 = 0 by a2;
then a6: Sum f = (Partial_Sums s) . (len f) by a5, XXREAL_3:4;
( Partial_Sums s is nonnegative & Partial_Sums s is non-decreasing ) by a7, MESFUNC9:16;
then Partial_Sums s is convergent by RINFSUP2:37;
then a9: ( (Partial_Sums s) ^\ (len f) is convergent & lim (Partial_Sums s) = lim ((Partial_Sums s) ^\ (len f)) ) by RINFSUP2:21;
defpred S₁[ Nat] means (Partial_Sums s) . (len f) = ((Partial_Sums s) ^\ (len f)) . $1;
(Partial_Sums s) . (len f) = (Partial_Sums s) . ((len f) + 0) ;
then b1: S₁[ 0 ] by NAT_1:def 3;
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 b3: S₁[k] ; :: thesis: S₁[k + 1]
(len f) + 0 < (len f) + (k + 1) by XREAL_1:6;
then not (len f) + (k + 1) in dom f by FINSEQ_3:25;
then b4: s . ((len f) + (k + 1)) = 0 by a2;
((Partial_Sums s) ^\ (len f)) . (k + 1) = (Partial_Sums s) . ((len f) + (k + 1)) by NAT_1:def 3
.= ((Partial_Sums s) . ((len f) + k)) + (s . (((len f) + k) + 1)) by MESFUNC9:def 1
.= (((Partial_Sums s) ^\ (len f)) . k) + 0 by b4, NAT_1:def 3 ;
hence S₁[k + 1] by b3, XXREAL_3:4; :: thesis: verum

end;

b5: for k being Nat holds S₁[k] from NAT_1:sch 2(b1, b2);
c1: (Partial_Sums s) . (len f) >= 0 by a7, SUPINF_2:51;

per cases ( (Partial_Sums s) . (len f) = +infty or (Partial_Sums s) . (len f) <> +infty ) ;

suppose c2: (Partial_Sums s) . (len f) = +infty ; :: thesis: ( Sum f = Sum s & Sum f = SUM s )

then for k being Element of NAT holds ((Partial_Sums s) ^\ (len f)) . k >= +infty by b5;
then (Partial_Sums s) ^\ (len f) is convergent_to_+infty by RINFSUP2:32;
then lim ((Partial_Sums s) ^\ (len f)) = +infty by MESFUNC5:def 12;
hence Sum s = Sum f by a6, c2, a9, MESFUNC9:def 3; :: thesis: Sum f = SUM s
hence SUM s = Sum f by a7, MEASURE8:2; :: thesis: verum

end;

suppose (Partial_Sums s) . (len f) <> +infty ; :: thesis: ( Sum f = Sum s & Sum f = SUM s )

then (Partial_Sums s) . (len f) in REAL by c1, XXREAL_0:14;
then reconsider r = (Partial_Sums s) . (len f) as Real ;
for k being Nat holds ((Partial_Sums s) ^\ (len f)) . k = r by b5;
then lim (Partial_Sums s) = Sum f by a6, a9, MESFUNC5:52;
hence Sum s = Sum f by MESFUNC9:def 3; :: thesis: Sum f = SUM s
hence SUM s = Sum f by a7, MEASURE8:2; :: thesis: verum

end;

end;