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:
assume that
A1: E = dom (F . 0) and
A2: F . 0 is nonnegative and
A3: F is with_the_same_dom and
A4: for n being Nat holds F . n is_measurable_on E and
A5: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x <= (F . m) . x and
A6: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
A7: lim F is_measurable_on E by A1, A3, A4, A6, MESFUNC8:25;
A8: for n being Nat holds F . n is nonnegative

proof

let n be Nat; :: thesis:
for x being set st x in dom (F . n) holds
0 <= (F . n) . x

proof

let x be set ; :: thesis:
assume x in dom (F . n) ; :: thesis:
then x in E by A1, A3, MESFUNC8:def 2;
then (F . 0) . x <= (F . n) . x by A5;
hence 0 <= (F . n) . x by A2, SUPINF_2:51; :: thesis:

end;

hence F . n is nonnegative by SUPINF_2:52; :: thesis:

end;

per cases ;

suppose ex n being Nat st M . (E /\ (eq_dom ((F . n),+infty))) <> 0 ; :: thesis:

then consider N being Nat such that
A9: M . (E /\ (eq_dom ((F . N),+infty))) <> 0 ;
A10: E = dom (F . N) by A1, A3, MESFUNC8:def 2;
then reconsider EE = E /\ (eq_dom ((F . N),+infty)) as Element of S by A4, MESFUNC1:33;
A11: EE c= E by XBOOLE_1:17;
then A12: F . N is_measurable_on EE by A4, MESFUNC1:30;
EE c= dom (F . N) by A1, A3, A11, MESFUNC8:def 2;
then A13: EE = dom ((F . N) | EE) by RELAT_1:62;
then EE = (dom (F . N)) /\ EE by RELAT_1:61;
then A14: (F . N) | EE is_measurable_on EE by A12, MESFUNC5:42;

now

let x be set ; :: thesis:
assume A15: x in EE ; :: thesis:
then x in eq_dom ((F . N),+infty) by XBOOLE_0:def 4;
then (F . N) . x = +infty by MESFUNC1:def 15;
then ((F . N) | EE) . x = +infty by A13, A15, FUNCT_1:47;
hence x in eq_dom (((F . N) | EE),+infty) by A13, A15, MESFUNC1:def 15; :: thesis:

end;

then A16: EE c= eq_dom (((F . N) | EE),+infty) by TARSKI:def 3;
for x being set st x in eq_dom (((F . N) | EE),+infty) holds
x in EE by A13, MESFUNC1:def 15;
then eq_dom (((F . N) | EE),+infty) c= EE by TARSKI:def 3;
then EE = eq_dom (((F . N) | EE),+infty) by A16, XBOOLE_0:def 10;
then A17: M . (EE /\ (eq_dom (((F . N) | EE),+infty))) <> 0 by A9;
F . N is_measurable_on E by A4;
then A18: Integral (M,((F . N) | EE)) <= Integral (M,((F . N) | E)) by A8, A10, A11, MESFUNC5:93;
reconsider N1 = N as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . $1));
consider I being Function of NAT,ExtREAL such that
A19: for n being Element of NAT holds I . n = H₁(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
A20: 0 < M . (E /\ (eq_dom ((F . N),+infty))) by A9, SUPINF_2:51;
A21: for n being Nat holds I . n = Integral (M,(F . n))

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
I . n = Integral (M,(F . n1)) by A19;
hence I . n = Integral (M,(F . n)) ; :: thesis:

end;

take I ; :: thesis:
A22: dom (lim F) = dom (F . 0) by MESFUNC8:def 9;
for x being set st x in dom (lim F) holds
(lim F) . x >= 0

proof

let x be set ; :: thesis:
assume A23: x in dom (lim F) ; :: thesis:
then reconsider x1 = x as Element of X ;
for n being Nat holds (F # x1) . n >= 0

proof

let n be Nat; :: thesis:
A24: (F . 0) . x1 >= 0 by A2, SUPINF_2:51;
(F . n) . x1 >= (F . 0) . x1 by A1, A5, A22, A23;
hence (F # x1) . n >= 0 by A24, MESFUNC5:def 13; :: thesis:

end;

then lim (F # x1) >= 0 by A1, A6, A22, A23, Th10;
hence (lim F) . x >= 0 by A23, MESFUNC8:def 9; :: thesis:

end;

then A25: lim F is nonnegative by SUPINF_2:52;
A26: E = dom (lim F) by A1, MESFUNC8:def 9;
A27: EE c= E /\ (eq_dom ((lim F),+infty))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: x in EE ; :: thesis:
then reconsider x1 = x as Element of X ;
x in eq_dom ((F . N),+infty) by A28, XBOOLE_0:def 4;
then (F . N) . x1 = +infty by MESFUNC1:def 15;
then A29: (F # x1) . N = +infty by MESFUNC5:def 13;
A30: x in E by A28, XBOOLE_0:def 4;
for n, m being Element of NAT st m <= n holds
(F # x1) . m <= (F # x1) . n

proof

let n, m be Element of NAT ; :: thesis:
assume m <= n ; :: thesis:
then (F . m) . x1 <= (F . n) . x1 by A5, A30;
then (F # x1) . m <= (F . n) . x1 by MESFUNC5:def 13;
hence (F # x1) . m <= (F # x1) . n by MESFUNC5:def 13; :: thesis:

end;

then A31: F # x1 is non-decreasing by RINFSUP2:7;
then A32: (F # x1) ^\ N1 is non-decreasing by RINFSUP2:26;
((F # x1) ^\ N1) . 0 = (F # x1) . (0 + N) by NAT_1:def 3;
then for n being Element of NAT holds +infty <= ((F # x1) ^\ N1) . n by A29, A32, RINFSUP2:7;
then (F # x1) ^\ N1 is convergent_to_+infty by RINFSUP2:32;
then A33: lim ((F # x1) ^\ N1) = +infty by Th7;
A34: sup (F # x1) = sup ((F # x1) ^\ N1) by A31, RINFSUP2:26;
lim (F # x1) = sup (F # x1) by A31, RINFSUP2:37;
then lim (F # x1) = +infty by A32, A34, A33, RINFSUP2:37;
then (lim F) . x1 = +infty by A1, A22, A30, MESFUNC8:def 9;
then x in eq_dom ((lim F),+infty) by A26, A30, MESFUNC1:def 15;
hence x in E /\ (eq_dom ((lim F),+infty)) by A30, XBOOLE_0:def 4; :: thesis:

end;

A35: for n, m being Element of NAT st m <= n holds
I . m <= I . n

proof

let n, m be Element of NAT ; :: thesis:
A36: F . m is_measurable_on E by A4;
assume m <= n ; :: thesis:
then A37: for x being Element of X st x in E holds
(F . m) . x <= (F . n) . x by A5;
A38: E = dom (F . m) by A1, A3, MESFUNC8:def 2;
A39: E = dom (F . n) by A1, A3, MESFUNC8:def 2;
F . n is_measurable_on E by A4;
then Integral (M,((F . m) | E)) <= Integral (M,((F . n) | E)) by A8, A38, A39, A36, A37, Th15;
then Integral (M,(F . m)) <= Integral (M,((F . n) | E)) by A38, RELAT_1:68;
then Integral (M,(F . m)) <= Integral (M,(F . n)) by A39, RELAT_1:68;
then I . m <= Integral (M,(F . n)) by A19;
hence I . m <= I . n by A19; :: thesis:

end;

then A40: I is non-decreasing by RINFSUP2:7;
then A41: I ^\ N1 is non-decreasing by RINFSUP2:26;
F . N is nonnegative by A8;
then Integral (M,((F . N) | EE)) = +infty by A13, A14, A17, Th13, MESFUNC5:15;
then +infty <= Integral (M,(F . N)) by A10, A18, RELAT_1:69;
then A42: Integral (M,(F . N)) = +infty by XXREAL_0:4;
for k being Element of NAT holds +infty <= (I ^\ N1) . k

proof

let k be Element of NAT ; :: thesis:
I . N1 <= I . (N1 + k) by A35, NAT_1:12;
then I . N1 <= (I ^\ N1) . k by NAT_1:def 3;
hence +infty <= (I ^\ N1) . k by A42, A21; :: thesis:

end;

then I ^\ N1 is convergent_to_+infty by RINFSUP2:32;
then A43: lim (I ^\ N1) = +infty by Th7;
E /\ (eq_dom ((lim F),+infty)) is Element of S by A7, A26, MESFUNC1:33;
then A44: M . (E /\ (eq_dom ((lim F),+infty))) <> 0 by A27, A20, MEASURE1:31;
A45: sup I = sup (I ^\ N1) by A40, RINFSUP2:26;
lim I = sup I by A40, RINFSUP2:37;
then lim I = +infty by A41, A45, A43, RINFSUP2:37;
hence ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I ) by A7, A21, A40, A26, A25, A44, Th13, RINFSUP2:37; :: thesis:

end;

suppose A46: for n being Nat holds M . (E /\ (eq_dom ((F . n),+infty))) = 0 ; :: thesis:

defpred S₁[ Element of NAT , set ] means $2 = E /\ (eq_dom ((F . $1),+infty));
A47: for n being Element of NAT ex A being Element of S st S₁[n,A]

proof

let n be Element of NAT ; :: thesis:
E c= dom (F . n) by A1, A3, MESFUNC8:def 2;
then reconsider A = E /\ (eq_dom ((F . n),+infty)) as Element of S by A4, MESFUNC1:33;
take A ; :: thesis:
thus S₁[n,A] ; :: thesis:

end;

consider L being Function of NAT,S such that
A48: for n being Element of NAT holds S₁[n,L . n] from FUNCT_2:sch 3(A47);
A49: rng L c= S by RELAT_1:def 19;
rng L is N_Sub_set_fam of X by MEASURE1:23;
then reconsider E0 = rng L as N_Measure_fam of S by A49, MEASURE2:def 1;
set E1 = E \ (union E0);
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL:] = (F . $1) | (E \ (union E0));
consider H being Functional_Sequence of X,ExtREAL such that
A50: for n being Nat holds H . n = H₁(n) from SEQFUNC:sch 1();
deffunc H₂( Element of NAT ) -> Element of ExtREAL = Integral (M,((F . $1) | (E \ (union E0))));
consider I being Function of NAT,ExtREAL such that
A51: for n being Element of NAT holds I . n = H₂(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
A52: E \ (union E0) c= E by XBOOLE_1:36;
then A53: for n being Nat holds F . n is_measurable_on E \ (union E0) by A4, MESFUNC1:30;
A54: for n being Nat holds
( dom (H . n) = E \ (union E0) & H . n is without-infty & H . n is without+infty )

proof

let n be Nat; :: thesis:
A55: dom (H . n) = dom ((F . n) | (E \ (union E0))) by A50;
E \ (union E0) c= dom (F . n) by A1, A3, A52, MESFUNC8:def 2;
hence dom (H . n) = E \ (union E0) by A55, RELAT_1:62; :: thesis:
(F . n) | (E \ (union E0)) is nonnegative by A8, MESFUNC5:15;
then H . n is nonnegative by A50;
hence H . n is without-infty by MESFUNC5:12; :: thesis:
for x being set st x in dom (H . n) holds
(H . n) . x < +infty

proof

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
let x be set ; :: thesis:
A56: L . n = E /\ (eq_dom ((F . n1),+infty)) by A48;
dom L = NAT by FUNCT_2:def 1;
then A57: L . n in rng L by A56, FUNCT_1:3;
assume x in dom (H . n) ; :: thesis:
then A58: x in dom ((F . n) | (E \ (union E0))) by A50;
then A59: x in E \ (union E0) by RELAT_1:57;
A60: x in dom (F . n) by A58, RELAT_1:57;
assume A61: (H . n) . x >= +infty ; :: thesis:
(H . n) . x = ((F . n) | (E \ (union E0))) . x by A50;
then (H . n) . x = (F . n) . x by A59, FUNCT_1:49;
then (F . n) . x = +infty by A61, XXREAL_0:4;
then x in eq_dom ((F . n),+infty) by A60, MESFUNC1:def 15;
then x in L . n by A52, A59, A56, XBOOLE_0:def 4;
then x in union E0 by A57, TARSKI:def 4;
hence contradiction by A59, XBOOLE_0:def 5; :: thesis:

end;

hence H . n is without+infty by MESFUNC5:11; :: thesis:

end;

for n, m being Nat holds dom (H . n) = dom (H . m)

proof

let n, m be Nat; :: thesis:
dom (H . n) = E \ (union E0) by A54;
hence dom (H . n) = dom (H . m) by A54; :: thesis:

end;

then reconsider H = H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
defpred S₂[ Element of NAT , set , set ] means $3 = (H . ($1 + 1)) - (H . $1);
A62: for n being Element of NAT
for x being set ex y being set st S₂[n,x,y] ;
consider G being Function such that
A63: ( dom G = NAT & G . 0 = H . 0 & ( for n being Element of NAT holds S₂[n,G . n,G . (n + 1)] ) ) from RECDEF_1:sch 1(A62);
A64: for n being Nat holds G . (n + 1) = (H . (n + 1)) - (H . n)

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
G . (n + 1) = (H . (n1 + 1)) - (H . n) by A63;
hence G . (n + 1) = (H . (n + 1)) - (H . n) ; :: thesis:

end;

now

defpred S₃[ Nat] means G . $1 is PartFunc of X,ExtREAL;
let f be set ; :: thesis:
assume f in rng G ; :: thesis:
then consider m being set such that
A65: m in dom G and
A66: f = G . m by FUNCT_1:def 3;
reconsider m = m as Nat by A63, A65;
A67: 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 A64;
hence S₃[n + 1] ; :: thesis:

end;

A68: S₃[ 0 ] by A63;
for n being Nat holds S₃[n] from NAT_1:sch 2(A68, A67);
then G . m is PartFunc of X,ExtREAL ;
hence f in PFuncs (X,ExtREAL) by A66, PARTFUN1:45; :: thesis:

end;

then rng G c= PFuncs (X,ExtREAL) by TARSKI:def 3;
then reconsider G = G as Functional_Sequence of X,ExtREAL by A63, FUNCT_2:def 1, RELSET_1:4;
A69: for n being Nat holds dom (G . n) = E \ (union E0)

proof

let n be Nat; :: thesis:

now

assume n <> 0 ; :: thesis:
then consider k being Nat such that
A70: n = k + 1 by NAT_1:6;
A71: H . (k + 1) is without-infty by A54;
A72: H . k is without+infty by A54;
G . (k + 1) = (H . (k + 1)) - (H . k) by A64;
then dom (G . (k + 1)) = (dom (H . (k + 1))) /\ (dom (H . k)) by A71, A72, MESFUNC5:17;
then dom (G . (k + 1)) = (E \ (union E0)) /\ (dom (H . k)) by A54;
then dom (G . (k + 1)) = (E \ (union E0)) /\ (E \ (union E0)) by A54;
hence dom (G . n) = E \ (union E0) by A70; :: thesis:

end;

hence dom (G . n) = E \ (union E0) by A54, A63; :: thesis:

end;

A73: for n, m being Nat holds dom (G . n) = dom (G . m)

proof

let n, m be Nat; :: thesis:
dom (G . n) = E \ (union E0) by A69;
hence dom (G . n) = dom (G . m) by A69; :: thesis:

end;

A74: for n being Nat holds G . n is nonnegative

proof

let n be Nat; :: thesis:
A75: ( n <> 0 implies G . n is nonnegative )

proof

assume n <> 0 ; :: thesis:
then consider k being Nat such that
A76: n = k + 1 by NAT_1:6;
A77: G . (k + 1) = (H . (k + 1)) - (H . k) by A64;
for x being set st x in dom (G . (k + 1)) holds
0 <= (G . (k + 1)) . x

proof

let x be set ; :: thesis:
assume A78: x in dom (G . (k + 1)) ; :: thesis:
A79: dom (G . (k + 1)) = E \ (union E0) by A69;
(H . k) . x = ((F . k) | (E \ (union E0))) . x by A50;
then A80: (H . k) . x = (F . k) . x by A78, A79, FUNCT_1:49;
(H . (k + 1)) . x = ((F . (k + 1)) | (E \ (union E0))) . x by A50;
then A81: (H . (k + 1)) . x = (F . (k + 1)) . x by A78, A79, FUNCT_1:49;
(F . k) . x <= (F . (k + 1)) . x by A5, A52, A78, A79, NAT_1:11;
then ((H . (k + 1)) . x) - ((H . k) . x) >= 0 by A81, A80, XXREAL_3:40;
hence 0 <= (G . (k + 1)) . x by A77, A78, MESFUNC1:def 4; :: thesis:

end;

hence G . n is nonnegative by A76, SUPINF_2:52; :: thesis:

end;

( n = 0 implies G . n is nonnegative )

proof

assume A82: n = 0 ; :: thesis:
(F . n) | (E \ (union E0)) is nonnegative by A8, MESFUNC5:15;
hence G . n is nonnegative by A50, A63, A82; :: thesis:

end;

hence G . n is nonnegative by A75; :: thesis:

end;

A83: for n1 being set st n1 in NAT holds
H . n1 = (Partial_Sums G) . n1

proof

defpred S₃[ Nat] means H . $1 = (Partial_Sums G) . $1;
let n1 be set ; :: thesis:
assume n1 in NAT ; :: thesis:
then reconsider n = n1 as Nat ;
A84: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
A85: H . k is without+infty by A54;
A86: H . k is without-infty by A54;
A87: dom (G . (k + 1)) = E \ (union E0) by A69;
G . (k + 1) is without-infty by A74, MESFUNC5:12;
then dom ((G . (k + 1)) + (H . k)) = (dom (G . (k + 1))) /\ (dom (H . k)) by A86, MESFUNC5:16;
then dom ((G . (k + 1)) + (H . k)) = (E \ (union E0)) /\ (E \ (union E0)) by A54, A87;
then A88: dom (H . (k + 1)) = dom ((G . (k + 1)) + (H . k)) by A54;
A89: G . (k + 1) = (H . (k + 1)) - (H . k) by A64;
for x being Element of X st x in dom (H . (k + 1)) holds
(H . (k + 1)) . x = ((G . (k + 1)) + (H . k)) . x

proof

let x be Element of X; :: thesis:
A90: (H . k) . x <> +infty by A85, MESFUNC5:def 6;
(H . k) . x <> -infty by A86, MESFUNC5:def 5;
then (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = ((H . (k + 1)) . x) - (((H . k) . x) - ((H . k) . x)) by A90, XXREAL_3:32;
then (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = ((H . (k + 1)) . x) - 0. by XXREAL_3:7;
then A91: (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = (H . (k + 1)) . x by XXREAL_3:4;
assume A92: x in dom (H . (k + 1)) ; :: thesis:
then x in E \ (union E0) by A54;
then (H . (k + 1)) . x = ((G . (k + 1)) . x) + ((H . k) . x) by A89, A87, A91, MESFUNC1:def 4;
hence (H . (k + 1)) . x = ((G . (k + 1)) + (H . k)) . x by A88, A92, MESFUNC1:def 3; :: thesis:

end;

then A93: H . (k + 1) = (G . (k + 1)) + (H . k) by A88, PARTFUN1:5;
assume S₃[k] ; :: thesis:
hence S₃[k + 1] by A93, Def4; :: thesis:

end;

A94: S₃[ 0 ] by A63, Def4;
for k being Nat holds S₃[k] from NAT_1:sch 2(A94, A84);
then H . n = (Partial_Sums G) . n ;
hence H . n1 = (Partial_Sums G) . n1 ; :: thesis:

end;

then A95: for n being Nat holds
( H . n = (Partial_Sums G) . n & lim H = lim (Partial_Sums G) ) by FUNCT_2:12;
reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A73, MESFUNC8:def 2;
reconsider G = G as with_the_same_dom additive Functional_Sequence of X,ExtREAL by A74, Th30;
A96: for k being Nat holds H . k is real-valued

proof

let k be Nat; :: thesis:
for x being Element of X st x in dom (H . k) holds
|.((H . k) . x).| < +infty

proof

let x be Element of X; :: thesis:
assume x in dom (H . k) ; :: thesis:
H . k is without+infty by A54;
then A97: (H . k) . x < +infty by MESFUNC5:def 6;
H . k is without-infty by A54;
then -infty < (H . k) . x by MESFUNC5:def 5;
hence |.((H . k) . x).| < +infty by A97, EXTREAL2:29, XXREAL_0:4; :: thesis:

end;

hence H . k is real-valued by MESFUNC2:def 1; :: thesis:

end;

A98: for n being Nat holds G . n is_measurable_on E \ (union E0)

proof

let n be Nat; :: thesis:
( n <> 0 implies G . n is_measurable_on E \ (union E0) )

proof

assume n <> 0 ; :: thesis:
then consider k being Nat such that
A99: n = k + 1 by NAT_1:6;
A100: E \ (union E0) = dom (H . k) by A54;
A101: G . (k + 1) = (H . (k + 1)) - (H . k) by A64;
A102: H . k is real-valued by A96;
A103: H . k is_measurable_on E \ (union E0) by A1, A3, A53, A50, Th20, XBOOLE_1:36;
A104: H . (k + 1) is real-valued by A96;
H . (k + 1) is_measurable_on E \ (union E0) by A1, A3, A53, A50, Th20, XBOOLE_1:36;
hence G . n is_measurable_on E \ (union E0) by A99, A103, A100, A104, A102, A101, MESFUNC2:11; :: thesis:

end;

hence G . n is_measurable_on E \ (union E0) by A1, A3, A52, A53, A50, A63, Th20; :: thesis:

end;

A105: E \ (union E0) = dom (G . 0) by A54, A63;
for x being Element of X st x in E \ (union E0) holds
G # x is summable

proof

let x be Element of X; :: thesis:
assume A106: x in E \ (union E0) ; :: thesis:
E \ (union E0) c= E by XBOOLE_1:36;
then F # x is convergent by A6, A106;
then H # x is convergent by A50, A106, Th12;
then (Partial_Sums G) # x is convergent by A83, FUNCT_2:12;
then Partial_Sums (G # x) is convergent by A105, A106, Th33;
hence G # x is summable by Def2; :: thesis:

end;

then consider J being ExtREAL_sequence such that
A107: for n being Nat holds J . n = Integral (M,((G . n) | (E \ (union E0)))) and
J is summable and
A108: Integral (M,((lim (Partial_Sums G)) | (E \ (union E0)))) = Sum J by A74, A105, A98, Th51;
for n being set st n in NAT holds
I . n = (Partial_Sums J) . n

proof

let n be set ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n1 = n as Element of NAT ;
A109: for n being Nat holds J . n = Integral (M,(G . n))

proof

let n be Nat; :: thesis:
dom (G . n) = E \ (union E0) by A69;
then (G . n) | (E \ (union E0)) = G . n by RELAT_1:68;
hence J . n = Integral (M,(G . n)) by A107; :: thesis:

end;

E \ (union E0) = dom (G . 0) by A69;
then (Partial_Sums J) . n1 = Integral (M,((Partial_Sums G) . n1)) by A74, A98, A109, Th46;
then (Partial_Sums J) . n1 = Integral (M,(H . n1)) by A83;
then (Partial_Sums J) . n1 = Integral (M,((F . n1) | (E \ (union E0)))) by A50;
hence I . n = (Partial_Sums J) . n by A51; :: thesis:

end;

then A110: I = Partial_Sums J by FUNCT_2:12;
dom (lim (Partial_Sums G)) = dom (H . 0) by A95, MESFUNC8:def 9;
then dom (lim (Partial_Sums G)) = E \ (union E0) by A54;
then A111: lim I = Integral (M,(lim H)) by A95, A108, A110, RELAT_1:68;
take I ; :: thesis:
A112: for x being Element of X st x in E \ (union E0) holds
F # x is convergent

proof

let x be Element of X; :: thesis:
A113: E \ (union E0) c= E by XBOOLE_1:36;
assume x in E \ (union E0) ; :: thesis:
hence F # x is convergent by A6, A113; :: thesis:

end;

A114: for n being Element of NAT st 0 <= n holds
(M * L) . n = 0

proof

let n be Element of NAT ; :: thesis:
assume 0 <= n ; :: thesis:
dom L = NAT by FUNCT_2:def 1;
then (M * L) . n = M . (L . n) by FUNCT_1:13;
then (M * L) . n = M . (E /\ (eq_dom ((F . n),+infty))) by A48;
hence (M * L) . n = 0 by A46; :: thesis:

end;

M * L is nonnegative by MEASURE2:1;
then SUM (M * L) = (Ser (M * L)) . 0 by A114, SUPINF_2:48;
then SUM (M * L) = (M * L) . 0 by SUPINF_2:44;
then SUM (M * L) = 0 by A114;
then M . (union E0) <= 0 by MEASURE2:11;
then A115: M . (union E0) = 0 by SUPINF_2:51;
A116: for n being Nat holds I . n = Integral (M,(F . n))

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A117: I . n = Integral (M,((F . n1) | (E \ (union E0)))) by A51;
dom (F . n) = E by A1, A3, MESFUNC8:def 2;
hence I . n = Integral (M,(F . n)) by A4, A115, A117, MESFUNC5:95; :: thesis:

end;

for n, m being Element of NAT st m <= n holds
I . m <= I . n

proof

let n, m be Element of NAT ; :: thesis:
A118: F . m is nonnegative by A8;
A119: dom (F . m) = E by A1, A3, MESFUNC8:def 2;
assume m <= n ; :: thesis:
then A120: for x being Element of X st x in dom (F . m) holds
(F . m) . x <= (F . n) . x by A5, A119;
A121: dom (F . n) = E by A1, A3, MESFUNC8:def 2;
A122: F . n is_measurable_on E by A4;
A123: F . n is nonnegative by A8;
F . m is_measurable_on E by A4;
then integral+ (M,(F . m)) <= integral+ (M,(F . n)) by A119, A121, A120, A118, A123, A122, MESFUNC5:85;
then Integral (M,(F . m)) <= integral+ (M,(F . n)) by A4, A119, A118, MESFUNC5:88;
then Integral (M,(F . m)) <= Integral (M,(F . n)) by A4, A121, A123, MESFUNC5:88;
then I . m <= Integral (M,(F . n)) by A116;
hence I . m <= I . n by A116; :: thesis:

end;

then A124: I is non-decreasing by RINFSUP2:7;
E = dom (lim F) by A1, MESFUNC8:def 9;
then A125: Integral (M,(lim F)) = Integral (M,((lim F) | (E \ (union E0)))) by A7, A115, MESFUNC5:95;
E \ (union E0) c= dom (F . 0) by A1, XBOOLE_1:36;
hence ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I ) by A125, A50, A116, A124, A112, A111, Th19, RINFSUP2:37; :: thesis:

end;