let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let A be Element of S; :: thesis:
let E be SetSequence of S; :: thesis:
assume that
A1: f is A -measurable and
A2: A = dom f and
A3: E is non-descending and
A4: lim E c= A and
A5: M . (A \ (lim E)) = 0 and
A6: ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) ; :: thesis:
Union E is Element of S by PROB_1:17;
then reconsider LE = lim E as Element of S by A3, SETLIM_1:80;
A \ (A \ LE) = A /\ LE by XBOOLE_1:48
.= LE by A4, XBOOLE_1:28 ;
then A7: Integral (M,f) = Integral (M,(f | LE)) by A1, A2, A5, MESFUNC5:95;
reconsider F = Partial_Diff_Union E as SetSequence of S ;
set g = f | LE;
A8: LE = (dom f) /\ LE by A2, A4, XBOOLE_1:28;
f is LE -measurable by A1, A4, MESFUNC1:30;
then A9: f | LE is LE -measurable by A8, MESFUNC5:42;
A10: lim E = Union E by A3, SETLIM_1:80;
then A11: LE = Union F by PROB_3:20;
A12: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
A13: ( (max+ f) | A = max+ (f | A) & (max- f) | A = max- (f | A) & (max+ f) | LE = max+ (f | LE) & (max- f) | LE = max- (f | LE) ) by MESFUNC5:28;
( dom (max+ f) = dom f & dom (max- f) = dom f ) by MESFUNC2:def 2, MESFUNC2:def 3;
then ( integral+ (M,((max+ f) | LE)) <= integral+ (M,((max+ f) | A)) & integral+ (M,((max- f) | LE)) <= integral+ (M,((max- f) | A)) ) by A2, A4, A12, A1, MESFUNC2:25, MESFUNC2:26, MESFUNC5:83;
then A14: ( integral+ (M,(max+ (f | LE))) < +infty or integral+ (M,(max- (f | LE))) < +infty ) by A2, A6, A13, XXREAL_0:2;
A15: LE = dom (f | LE) by A8, RELAT_1:61;
then consider J being ExtREAL_sequence such that
A16: for n being Nat holds J . n = Integral (M,((f | LE) | (F . n))) and
A17: ( J is summable & Integral (M,(f | LE)) = Sum J ) by A9, A11, A14, Th17;
reconsider I = Partial_Sums J as ExtREAL_sequence ;
take I ; :: thesis:
A18: for n being Nat holds (f | LE) | ((Partial_Union F) . n) = f | ((Partial_Union E) . n)

proof

let n be Nat; :: thesis:
A19: (Partial_Union F) . n = (Partial_Union E) . n by PROB_3:19;

now :: thesis:

let x be object ; :: thesis:
assume x in (Partial_Union E) . n ; :: thesis:
then consider k being Nat such that
A20: ( k <= n & x in E . k ) by PROB_3:13;
k in NAT by ORDINAL1:def 12;
then k in dom E by FUNCT_2:def 1;
then E . k c= union (rng E) by FUNCT_1:3, ZFMISC_1:74;
then E . k c= Union E by CARD_3:def 4;
hence x in Union E by A20; :: thesis:

end;

then (Partial_Union E) . n c= LE by A10;
hence (f | LE) | ((Partial_Union F) . n) = f | ((Partial_Union E) . n) by A19, RELAT_1:74; :: thesis:

end;

A21: for n being Nat holds (Partial_Union E) . n c= Union E

proof

let n be Nat; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in (Partial_Union E) . n ; :: thesis:
then consider k being Nat such that
A22: ( k <= n & x in E . k ) by PROB_3:13;
k in NAT by ORDINAL1:def 12;
then k in dom E by FUNCT_2:def 1;
then E . k in rng E by FUNCT_1:3;
then x in union (rng E) by A22, TARSKI:def 4;
hence x in Union E by CARD_3:def 4; :: thesis:

end;

hence (Partial_Union E) . n c= Union E ; :: thesis:

end;

defpred S₁[ Nat] means I . $1 = Integral (M,((f | LE) | ((Partial_Union F) . $1)));
I . 0 = J . 0 by MESFUNC9:def 1
.= Integral (M,((f | LE) | (F . 0))) by A16 ;
then A23: S₁[ 0 ] by PROB_3:def 2;
A24: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

end;

A34: for n being Nat holds S₁[n] from NAT_1:sch 2(A23, A24);
thus for n being Nat holds I . n = Integral (M,(f | ((Partial_Union E) . n))) :: thesis:

proof

let n be Nat; :: thesis:
I . n = Integral (M,((f | LE) | ((Partial_Union F) . n))) by A34;
hence I . n = Integral (M,(f | ((Partial_Union E) . n))) by A18; :: thesis:

end;

thus I is convergent by A17, MESFUNC9:def 2; :: thesis:
thus Integral (M,f) = lim I by A7, A17, MESFUNC9:def 3; :: thesis: