let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
assume that
A1: E c= dom f and
A2: f is nonnegative and
A3: f is E -measurable ; :: thesis:
set F = f | E;
A4: dom (f | E) = E by A1, RELAT_1:62;
E = (dom f) /\ E by A1, XBOOLE_1:28;
then f | E is E -measurable by A3, MESFUNC5:42;
then consider h being Functional_Sequence of X,ExtREAL such that
A5: for n being Nat holds
( h . n is_simple_func_in S & dom (h . n) = dom (f | E) ) and
A6: for n being Nat holds h . n is nonnegative and
A7: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | E) holds
(h . n) . x <= (h . m) . x and
A8: for x being Element of X st x in dom (f | E) holds
( h # x is convergent & lim (h # x) = (f | E) . x ) by A2, A4, MESFUNC5:15, MESFUNC5:64;
defpred S₁[ Nat, set , set ] means $3 = (h . ($1 + 1)) - (h . $1);
A9: for n being Nat
for x being set ex y being set st S₁[n,x,y] ;
consider g being Function such that
A10: ( dom g = NAT & g . 0 = h . 0 & ( for n being Nat holds S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 1(A9);

now :: thesis:

defpred S₂[ Nat] means g . $1 is PartFunc of X,ExtREAL;
let f be object ; :: thesis:
assume f in rng g ; :: thesis:
then consider m being object such that
A11: m in dom g and
A12: f = g . m by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A10, A11;
A13: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume S₂[n] ; :: thesis:
g . (n + 1) = (h . (n + 1)) - (h . n) by A10;
hence S₂[n + 1] ; :: thesis:

end;

A14: S₂[ 0 ] by A10;
for n being Nat holds S₂[n] from NAT_1:sch 2(A14, A13);
then g . m is PartFunc of X,ExtREAL ;
hence f in PFuncs (X,ExtREAL) by A12, PARTFUN1:45; :: thesis:

end;

then rng g c= PFuncs (X,ExtREAL) ;
then reconsider g = g as Functional_Sequence of X,ExtREAL by A10, FUNCT_2:def 1, RELSET_1:4;
take g ; :: thesis:
A15: for n being Nat holds
( g . n is_simple_func_in S & g . n is nonnegative & g . n is E -measurable & E c= dom (g . n) )

proof

let n be Nat; :: thesis:

per cases ;

suppose A16: n = 0 ; :: thesis:

hence ( g . n is_simple_func_in S & g . n is nonnegative ) by A5, A6, A10; :: thesis:
hence g . n is E -measurable by MESFUNC2:34; :: thesis:
thus E c= dom (g . n) by A4, A5, A10, A16; :: thesis:

end;

suppose n <> 0 ; :: thesis:

then consider m being Nat such that
A17: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A18: g . n = (h . n) - (h . m) by A10, A17;
then A19: g . n = (h . n) + (- (h . m)) by MESFUNC2:8;
A20: h . n is_simple_func_in S by A5;
then A21: h . n is without-infty by MESFUNC5:14;
A22: dom (h . n) = dom (f | E) by A5;
(- jj) (#) (h . m) is_simple_func_in S by A5, MESFUNC5:39;
then A23: - (h . m) is_simple_func_in S by MESFUNC2:9;
hence g . n is_simple_func_in S by A19, A20, MESFUNC5:38; :: thesis:
A24: h . m is_simple_func_in S by A5;
then h . m is without+infty by MESFUNC5:14;
then A25: dom ((h . n) - (h . m)) = (dom (h . n)) /\ (dom (h . m)) by A21, MESFUNC5:17;
A26: dom (h . m) = dom (f | E) by A5;
then for x being object st x in dom ((h . n) - (h . m)) holds
(h . m) . x <= (h . n) . x by A7, A17, A25, A22, NAT_1:11;
hence g . n is nonnegative by A18, A20, A24, MESFUNC5:40; :: thesis:
thus g . n is E -measurable by A19, A20, A23, MESFUNC2:34, MESFUNC5:38; :: thesis:
thus E c= dom (g . n) by A4, A10, A17, A25, A22, A26; :: thesis:

end;

hence A27: g is additive by Th35; :: thesis:
thus for n being Nat holds
( g . n is_simple_func_in S & g . n is nonnegative & g . n is E -measurable ) by A15; :: thesis:

A28: now :: thesis:

let x be Element of X; :: thesis:
assume A29: x in E ; :: thesis:
then A30: h # x is convergent by A4, A8;
A31: for m being Nat holds (Partial_Sums (g # x)) . m = (h # x) . m

proof

defpred S₂[ Nat] means (Partial_Sums (g # x)) . $1 = (h # x) . $1;
let m be Nat; :: thesis:
A32: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

set Pgx = Partial_Sums (g # x);
let k be Nat; :: thesis:
assume S₂[k] ; :: thesis:
then A33: (Partial_Sums (g # x)) . k = (h . k) . x by MESFUNC5:def 13;
A34: dom (h . (k + 1)) = dom (f | E) by A5;
A35: h . (k + 1) is_simple_func_in S by A5;
then A36: h . (k + 1) is without-infty by MESFUNC5:14;
then A37: -infty < (h . (k + 1)) . x ;
h . (k + 1) is without+infty by A35, MESFUNC5:14;
then A38: (h . (k + 1)) . x < +infty ;
A39: dom (h . k) = dom (f | E) by A5;
A40: h . k is_simple_func_in S by A5;
then A41: h . k is without+infty by MESFUNC5:14;
then A42: (h . k) . x < +infty ;
h . k is without-infty by A40, MESFUNC5:14;
then A43: -infty < (h . k) . x ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
reconsider hk1x = (h . (k + 1)) . x as Element of REAL by A37, A38, XXREAL_0:14;
A44: g . (k + 1) = (h . (k + 1)) - (h . k) by A10;
reconsider hkx = (h . k) . x as Element of REAL by A43, A42, XXREAL_0:14;
((h . (k + 1)) . x) - ((h . k) . x) = hk1x - hkx by SUPINF_2:3;
then A45: (((h . (k + 1)) . x) - ((h . k) . x)) + ((h . k) . x) = (hk1x - hkx) + hkx by SUPINF_2:1;
(Partial_Sums (g # x)) . (k + 1) = ((Partial_Sums (g # x)) . k) + ((g # x) . (k + 1)) by Def1;
then A46: (Partial_Sums (g # x)) . (k + 1) = ((h . k) . x) + ((g . (k + 1)) . x) by A33, MESFUNC5:def 13;
dom ((h . (k + 1)) - (h . k)) = (dom (h . (k + 1))) /\ (dom (h . k)) by A36, A41, MESFUNC5:17;
then (g . (k + 1)) . x = ((h . (k + 1)) . x) - ((h . k) . x) by A4, A29, A34, A39, A44, MESFUNC1:def 4;
hence S₂[k + 1] by A46, A45, MESFUNC5:def 13; :: thesis:

end;

(Partial_Sums (g # x)) . 0 = (g # x) . 0 by Def1;
then (Partial_Sums (g # x)) . 0 = (g . 0) . x by MESFUNC5:def 13;
then A47: S₂[ 0 ] by A10, MESFUNC5:def 13;
for k being Nat holds S₂[k] from NAT_1:sch 2(A47, A32);
hence (Partial_Sums (g # x)) . m = (h # x) . m ; :: thesis:

end;

A48: lim (h # x) = (f | E) . x by A4, A8, A29;

per cases by A30;

suppose A49: h # x is convergent_to_finite_number ; :: thesis:

then A50: not h # x is convergent_to_-infty by MESFUNC5:51;
not h # x is convergent_to_+infty by A49, MESFUNC5:50;
then consider s being Real such that
A51: lim (h # x) = s and
A52: for p being Real st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
|.(((h # x) . m) - (lim (h # x))).| < p and
h # x is convergent_to_finite_number by A30, A50, MESFUNC5:def 12;
for p being Real st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
|.(((Partial_Sums (g # x)) . m) - s).| < p

proof

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider N being Nat such that
A53: for m being Nat st N <= m holds
|.(((h # x) . m) - (lim (h # x))).| < p by A52;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then |.(((h # x) . m) - (lim (h # x))).| < p by A53;
hence |.(((Partial_Sums (g # x)) . m) - s).| < p by A31, A51; :: thesis:

end;

then A54: Partial_Sums (g # x) is convergent_to_finite_number ;
then A55: Partial_Sums (g # x) is convergent ;
hence g # x is summable ; :: thesis:
for p being Real st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
|.(((Partial_Sums (g # x)) . m) - (lim (h # x))).| < p

proof

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider N being Nat such that
A56: for m being Nat st N <= m holds
|.(((h # x) . m) - (lim (h # x))).| < p by A52;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then |.(((h # x) . m) - (lim (h # x))).| < p by A56;
hence |.(((Partial_Sums (g # x)) . m) - (lim (h # x))).| < p by A31; :: thesis:

end;

then lim (Partial_Sums (g # x)) = lim (h # x) by A51, A54, A55, MESFUNC5:def 12;
hence Sum (g # x) = f . x by A29, A48, FUNCT_1:49; :: thesis:

end;

suppose A57: h # x is convergent_to_+infty ; :: thesis:

for p being Real st 0 < p holds
ex N being Nat st
for m being Nat st N <= m holds
p <= (Partial_Sums (g # x)) . m

proof

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider N being Nat such that
A58: for m being Nat st N <= m holds
p <= (h # x) . m by A57;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then p <= (h # x) . m by A58;
hence p <= (Partial_Sums (g # x)) . m by A31; :: thesis:

end;

then A59: Partial_Sums (g # x) is convergent_to_+infty ;
then A60: Partial_Sums (g # x) is convergent ;
then A61: lim (Partial_Sums (g # x)) = +infty by A59, MESFUNC5:def 12;
thus g # x is summable by A60; :: thesis:
lim (h # x) = +infty by A30, A57, MESFUNC5:def 12;
hence Sum (g # x) = f . x by A29, A48, A61, FUNCT_1:49; :: thesis:

end;

suppose A62: h # x is convergent_to_-infty ; :: thesis:

for p being Real st p < 0 holds
ex N being Nat st
for m being Nat st N <= m holds
(Partial_Sums (g # x)) . m <= p

proof

let p be Real; :: thesis:
assume p < 0 ; :: thesis:
then consider N being Nat such that
A63: for m being Nat st N <= m holds
(h # x) . m <= p by A62;
take N ; :: thesis:
let m be Nat; :: thesis:
assume N <= m ; :: thesis:
then (h # x) . m <= p by A63;
hence (Partial_Sums (g # x)) . m <= p by A31; :: thesis:

end;

then A64: Partial_Sums (g # x) is convergent_to_-infty ;
then A65: Partial_Sums (g # x) is convergent ;
then A66: lim (Partial_Sums (g # x)) = -infty by A64, MESFUNC5:def 12;
thus g # x is summable by A65; :: thesis:
lim (h # x) = -infty by A30, A62, MESFUNC5:def 12;
hence Sum (g # x) = f . x by A29, A48, A66, FUNCT_1:49; :: thesis:

end;

hence for x being Element of X st x in E holds
( g # x is summable & f . x = Sum (g # x) ) ; :: thesis:

per cases ;

suppose E = {} ; :: thesis:

hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((g . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) by A1, A3, A15, Lm2; :: thesis:

end;

suppose A67: E <> {} ; :: thesis:

for m being Nat holds
( g . m is_simple_func_in S & g . m is nonnegative & g . m is E -measurable & E c= dom (g . m) ) by A15;
then E common_on_dom g by A67, SEQFUNC:def 9;
hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((g . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) by A1, A2, A3, A15, A27, A28, Lm3; :: thesis:

end;