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 Functional_Sequence of X,ExtREAL ; :: 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_measurable_on E & F is additive ) and
NE: E common_on_dom F and
A4: for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative ) and
A5: for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ; :: thesis:
B1: dom (f | E) = E by A1, RELAT_1:91;
P0: for n being Nat holds
( (F . n) | E is_simple_func_in S & (F . n) | E is nonnegative & dom ((F . n) | E) = E )

proof

let n be Nat; :: thesis:
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
P01: ( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n') ) by A4, NE, SEQFUNC:def 10;
hence (F . n) | E is_simple_func_in S by MESFUNC5:40; :: thesis:
thus (F . n) | E is nonnegative by P01, MESFUNC5:21; :: thesis:
thus dom ((F . n) | E) = E by P01, RELAT_1:91; :: thesis:

end;

deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (F . $1) | E;
consider g1 being Functional_Sequence of X,ExtREAL such that
G1: for n being Nat holds g1 . n = H₁(n) from SEQFUNC:sch 1();
set G = Partial_Sums g1;
deffunc H₂( Element of NAT ) -> Element of ExtREAL = Integral M,(g1 . $1);
consider I being ExtREAL_sequence such that
A6: for n being Element of NAT holds I . n = H₂(n) from FUNCT_2:sch 4();
take I ; :: thesis:
G2: for n being Nat holds I . n = Integral M,((F . n) | E)

proof

let n be Nat; :: thesis:
reconsider m = n as Element of NAT by ORDINAL1:def 13;
I . m = Integral M,(g1 . m) by A6;
hence I . n = Integral M,((F . n) | E) by G1; :: thesis:

end;

(Partial_Sums g1) . 0 = g1 . 0 by Def0;
then P10: (Partial_Sums g1) . 0 = (F . 0 ) | E by G1;
for n, m being Nat holds dom (g1 . n) = dom (g1 . m)

proof

let n, m be Nat; :: thesis:
R12: dom (g1 . n) = dom ((F . n) | E) by G1;
dom (g1 . m) = dom ((F . m) | E) by G1;
then dom (g1 . m) = E by P0;
hence dom (g1 . n) = dom (g1 . m) by P0, R12; :: thesis:

end;

then XX: g1 is with_the_same_dom by MESFUNC8:def 2;
T1: for k being Nat holds g1 . k is nonnegative

proof

let k be Nat; :: thesis:
(F . k) | E is nonnegative by P0;
hence g1 . k is nonnegative by G1; :: thesis:

end;

R1: for n being Nat holds
( (Partial_Sums g1) . n is_simple_func_in S & (Partial_Sums g1) . n is nonnegative & dom ((Partial_Sums g1) . n) = E )

proof

let n be Nat; :: thesis:
R10: for n being Nat holds g1 . n is_simple_func_in S

proof

let n be Nat; :: thesis:
(F . n) | E is_simple_func_in S by P0;
hence g1 . n is_simple_func_in S by G1; :: thesis:

end;

hence (Partial_Sums g1) . n is_simple_func_in S by Lem10; :: thesis:
thus (Partial_Sums g1) . n is nonnegative by T1, ADD3C; :: thesis:
R11: g1 is additive by R10, Lem10;
dom (g1 . 0 ) = dom ((F . 0 ) | E) by G1;
then dom (g1 . 0 ) = E by P0;
hence dom ((Partial_Sums g1) . n) = E by R11, XX, ADD0; :: thesis:

end;

set L = Partial_Sums I;
L3: for n being Nat holds integral' M,((Partial_Sums g1) . n) = (Partial_Sums I) . n

proof

let n be Nat; :: thesis:
reconsider m = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Element of NAT ] means (Partial_Sums I) . $1 = integral' M,((Partial_Sums g1) . $1);
(Partial_Sums I) . 0 = I . 0 by Def1;
then L31: (Partial_Sums I) . 0 = Integral M,((Partial_Sums g1) . 0 ) by P10, G2;
( (Partial_Sums g1) . 0 is_simple_func_in S & (Partial_Sums g1) . 0 is nonnegative ) by R1;
then L32: S₁[ 0 ] by L31, MESFUNC5:95;
L33: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume L4: S₁[k] ; :: thesis:
(Partial_Sums g1) . (k + 1) = ((Partial_Sums g1) . k) + (g1 . (k + 1)) by Def0;
then P15: (Partial_Sums g1) . (k + 1) = ((Partial_Sums g1) . k) + ((F . (k + 1)) | E) by G1;
(Partial_Sums I) . (k + 1) = ((Partial_Sums I) . k) + (I . (k + 1)) by Def1;
then L5: (Partial_Sums I) . (k + 1) = (integral' M,((Partial_Sums g1) . k)) + (Integral M,((F . (k + 1)) | E)) by G2, L4;
L7: ( (F . (k + 1)) | E is_simple_func_in S & (F . (k + 1)) | E is nonnegative ) by P0;
L8: ( (Partial_Sums g1) . k is_simple_func_in S & (Partial_Sums g1) . k is nonnegative & (Partial_Sums g1) . (k + 1) is_simple_func_in S & (Partial_Sums g1) . (k + 1) is nonnegative ) by R1;
L9: ( dom ((Partial_Sums g1) . k) = E & dom ((F . (k + 1)) | E) = E ) by P0, R1;
then E = (dom ((Partial_Sums g1) . k)) /\ (dom ((F . (k + 1)) | E)) ;
then dom (((Partial_Sums g1) . k) + ((F . (k + 1)) | E)) = E by L7, L8, MESFUNC5:71;
then L10: integral' M,(((Partial_Sums g1) . k) + ((F . (k + 1)) | E)) = (integral' M,(((Partial_Sums g1) . k) | E)) + (integral' M,(((F . (k + 1)) | E) | E)) by L7, L8, MESFUNC5:71;
( ((Partial_Sums g1) . k) | E = (Partial_Sums g1) . k & ((F . (k + 1)) | E) | E = (F . (k + 1)) | E ) by L9, RELAT_1:97;
hence S₁[k + 1] by P15, L7, L10, L5, MESFUNC5:95; :: thesis:

end;

L34: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(L32, L33);
n is Element of NAT by ORDINAL1:def 13;
hence integral' M,((Partial_Sums g1) . n) = (Partial_Sums I) . n by L34; :: thesis:

end;

C1: for x being Element of X st x in dom (f | E) holds
( g1 # x is summable & (f | E) . x = Sum (g1 # x) )

proof

let x be Element of X; :: thesis:
assume C11: x in dom (f | E) ; :: thesis:
then C12: ( F # x is summable & f . x = Sum (F # x) ) by A5, B1;
C14: f . x = (f | E) . x by C11, FUNCT_1:70;
for n being set st n in NAT holds
(F # x) . n = (g1 # x) . n

proof

let n be set ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n1 = n as Nat ;
C16: (F . n1) | E = g1 . n1 by G1;
dom ((F . n1) | E) = E by P0;
then C13: (g1 . n1) . x = (F . n1) . x by C11, C16, B1, FUNCT_1:70;
(F # x) . n = (F . n1) . x by MESFUNC5:def 13;
hence (F # x) . n = (g1 # x) . n by C13, MESFUNC5:def 13; :: thesis:

end;

hence ( g1 # x is summable & (f | E) . x = Sum (g1 # x) ) by C12, C14, FUNCT_2:18; :: thesis:

end;

X0: g1 is additive by A3, G1, Lem09;
g1 . 0 = (F . 0 ) | E by G1;
then Y1: dom (g1 . 0 ) = E by P0;
(dom f) /\ E = E by B1, RELAT_1:90;
then A7: ( f | E is_measurable_on E & f | E is nonnegative ) by A2, A3, MESFUNC5:21, MESFUNC5:48;
then consider F being Functional_Sequence of X,ExtREAL , K being ExtREAL_sequence such that
A8: ( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f | E) ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | E) holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom (f | E) holds
( F # x is convergent & lim (F # x) = (f | E) . x ) ) & ( for n being Nat holds K . n = integral' M,(F . n) ) & K is convergent & integral+ M,(f | E) = lim K ) by B1, MESFUNC5:def 15;
R2: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
((Partial_Sums g1) . n) . x <= ((Partial_Sums g1) . m) . x by XX, T1, Y1, ADD3D;
for x being Element of X st x in E holds
( F # x is convergent & (Partial_Sums g1) # x is convergent & lim (F # x) = lim ((Partial_Sums g1) # x) )

proof

let x be Element of X; :: thesis:
assume R31: x in E ; :: thesis:
hence F # x is convergent by B1, A8; :: thesis:
g1 # x is summable by R31, B1, C1;
then Partial_Sums (g1 # x) is convergent by Def2;
hence (Partial_Sums g1) # x is convergent by R31, Y1, X0, XX, Cor01; :: thesis:
( g1 # x is summable & (f | E) . x = Sum (g1 # x) ) by R31, B1, C1;
then lim ((Partial_Sums g1) # x) = (f | E) . x by B1, R31, Y1, X0, XX, Cor02;
hence lim (F # x) = lim ((Partial_Sums g1) # x) by B1, A8, R31; :: thesis:

end;

then ( Partial_Sums I is convergent & lim (Partial_Sums I) = integral+ M,(f | E) ) by R1, R2, B1, A8, L3, MESFUNC5:82;
hence ( ( for n being Nat holds I . n = Integral M,((F . n) | E) ) & I is summable & Integral M,(f | E) = Sum I ) by A7, B1, G2, Def2, MESFUNC5:94; :: thesis: