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 E -measurable 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 E -measurable 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 object st x in dom (F . n) holds
0 <= (F . n) . x

proof

let x be object ; :: thesis:
assume x in dom (F . n) ; :: thesis:
then x in E by A1, A3;
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;
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 EE -measurable by A4, MESFUNC1:30;
EE c= dom (F . N) by A1, A3, A11;
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 EE -measurable by A12, MESFUNC5:42;

now :: thesis:

let x be object ; :: 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) ;
for x being object 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 ;
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 E -measurable 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 sequence of 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 object st x in dom (lim F) holds
(lim F) . x >= 0

proof

let x be object ; :: 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 object ; :: 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 Nat st m <= n holds
(F # x1) . m <= (F # x1) . n

proof

let n, m be 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 Nat st m <= n holds
I . m <= I . n

proof

let n, m be Nat; :: thesis:
A36: F . m is E -measurable 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;
A39: E = dom (F . n) by A1, A3;
A40: n in NAT by ORDINAL1:def 12;
A41: m in NAT by ORDINAL1:def 12;
F . n is E -measurable 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;
then Integral (M,(F . m)) <= Integral (M,(F . n)) by A39;
then I . m <= Integral (M,(F . n)) by A19, A41;
hence I . m <= I . n by A19, A40; :: thesis:

end;

then A42: I is non-decreasing by RINFSUP2:7;
then A43: 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;
then A44: 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 A44, A21; :: thesis:

end;

then I ^\ N1 is convergent_to_+infty by RINFSUP2:32;
then A45: lim (I ^\ N1) = +infty by Th7;
E /\ (eq_dom ((lim F),+infty)) is Element of S by A7, A26, MESFUNC1:33;
then A46: M . (E /\ (eq_dom ((lim F),+infty))) <> 0 by A27, A20, MEASURE1:31;
A47: sup I = sup (I ^\ N1) by A42, RINFSUP2:26;
lim I = sup I by A42, RINFSUP2:37;
then lim I = +infty by A43, A47, A45, 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, A42, A26, A25, A46, Th13, RINFSUP2:37; :: thesis:

end;

suppose A48: 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));
A49: 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;
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 sequence of S such that
A50: for n being Element of NAT holds S₁[n,L . n] from FUNCT_2:sch 3(A49);
A51: 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 A51, 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
A52: 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 sequence of ExtREAL such that
A53: for n being Element of NAT holds I . n = H₂(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
A54: E \ (union E0) c= E by XBOOLE_1:36;
then A55: for n being Nat holds F . n is E \ (union E0) -measurable by A4, MESFUNC1:30;
A56: 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:
A57: dom (H . n) = dom ((F . n) | (E \ (union E0))) by A52;
E \ (union E0) c= dom (F . n) by A1, A3, A54;
hence dom (H . n) = E \ (union E0) by A57, RELAT_1:62; :: thesis:
(F . n) | (E \ (union E0)) is nonnegative by A8, MESFUNC5:15;
then H . n is nonnegative by A52;
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:
A58: L . n = E /\ (eq_dom ((F . n1),+infty)) by A50;
dom L = NAT by FUNCT_2:def 1;
then A59: L . n in rng L by A58, FUNCT_1:3;
assume x in dom (H . n) ; :: thesis:
then A60: x in dom ((F . n) | (E \ (union E0))) by A52;
then A61: x in E \ (union E0) by RELAT_1:57;
A62: x in dom (F . n) by A60, RELAT_1:57;
assume A63: (H . n) . x >= +infty ; :: thesis:
(H . n) . x = ((F . n) | (E \ (union E0))) . x by A52;
then (H . n) . x = (F . n) . x by A61, FUNCT_1:49;
then (F . n) . x = +infty by A63, XXREAL_0:4;
then x in eq_dom ((F . n),+infty) by A62, MESFUNC1:def 15;
then x in L . n by A54, A61, A58, XBOOLE_0:def 4;
then x in union E0 by A59, TARSKI:def 4;
hence contradiction by A61, 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 A56;
hence dom (H . n) = dom (H . m) by A56; :: thesis:

end;

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

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
A67: m in dom G and
A68: f = G . m by FUNCT_1:def 3;
reconsider m = m as Nat by A65, A67;
A69: 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 A66;
hence S₃[n + 1] ; :: thesis:

end;

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

end;

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

proof

let n be Nat; :: thesis:

now :: thesis:

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

end;

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

end;

A75: 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 A71;
hence dom (G . n) = dom (G . m) by A71; :: thesis:

end;

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

proof

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

proof

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

proof

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

end;

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

end;

( n = 0 implies G . n is nonnegative )

proof

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

end;

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

end;

A85: for n1 being object 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 object ; :: thesis:
assume n1 in NAT ; :: thesis:
then reconsider n = n1 as Nat ;
A86: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
A87: H . k is without+infty by A56;
A88: H . k is without-infty by A56;
A89: dom (G . (k + 1)) = E \ (union E0) by A71;
G . (k + 1) is without-infty by A76, MESFUNC5:12;
then dom ((G . (k + 1)) + (H . k)) = (dom (G . (k + 1))) /\ (dom (H . k)) by A88, MESFUNC5:16;
then dom ((G . (k + 1)) + (H . k)) = (E \ (union E0)) /\ (E \ (union E0)) by A56, A89;
then A90: dom (H . (k + 1)) = dom ((G . (k + 1)) + (H . k)) by A56;
A91: G . (k + 1) = (H . (k + 1)) - (H . k) by A66;
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:
A92: (H . k) . x <> +infty by A87;
(H . k) . x <> -infty by A88;
then (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = ((H . (k + 1)) . x) - (((H . k) . x) - ((H . k) . x)) by A92, XXREAL_3:32;
then (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = ((H . (k + 1)) . x) - 0. by XXREAL_3:7;
then A93: (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = (H . (k + 1)) . x by XXREAL_3:4;
assume A94: x in dom (H . (k + 1)) ; :: thesis:
then x in E \ (union E0) by A56;
then (H . (k + 1)) . x = ((G . (k + 1)) . x) + ((H . k) . x) by A91, A89, A93, MESFUNC1:def 4;
hence (H . (k + 1)) . x = ((G . (k + 1)) + (H . k)) . x by A90, A94, MESFUNC1:def 3; :: thesis:

end;

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

end;

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

end;

then A97: 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 A75, MESFUNC8:def 2;
reconsider G = G as with_the_same_dom additive Functional_Sequence of X,ExtREAL by A76, Th30;
A98: 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 A56;
then A99: (H . k) . x < +infty ;
H . k is without-infty by A56;
then -infty < (H . k) . x ;
hence |.((H . k) . x).| < +infty by A99, EXTREAL1:40, XXREAL_0:4; :: thesis:

end;

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

end;

A100: for n being Nat holds G . n is E \ (union E0) -measurable

proof

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

proof

assume n <> 0 ; :: thesis:
then consider k being Nat such that
A101: n = k + 1 by NAT_1:6;
A102: E \ (union E0) = dom (H . k) by A56;
A103: G . (k + 1) = (H . (k + 1)) - (H . k) by A66;
A104: H . k is real-valued by A98;
A105: H . k is E \ (union E0) -measurable by A1, A3, A55, A52, Th20, XBOOLE_1:36;
A106: H . (k + 1) is real-valued by A98;
H . (k + 1) is E \ (union E0) -measurable by A1, A3, A55, A52, Th20, XBOOLE_1:36;
hence G . n is E \ (union E0) -measurable by A101, A105, A102, A106, A104, A103, MESFUNC2:11; :: thesis:

end;

hence G . n is E \ (union E0) -measurable by A1, A3, A54, A55, A52, A65, Th20; :: thesis:

end;

A107: E \ (union E0) = dom (G . 0) by A56, A65;
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 A108: x in E \ (union E0) ; :: thesis:
E \ (union E0) c= E by XBOOLE_1:36;
then F # x is convergent by A6, A108;
then H # x is convergent by A52, A108, Th12;
then (Partial_Sums G) # x is convergent by A85, FUNCT_2:12;
then Partial_Sums (G # x) is convergent by A107, A108, Th33;
hence G # x is summable ; :: thesis:

end;

then consider J being ExtREAL_sequence such that
A109: for n being Nat holds J . n = Integral (M,((G . n) | (E \ (union E0)))) and
J is summable and
A110: Integral (M,((lim (Partial_Sums G)) | (E \ (union E0)))) = Sum J by A76, A107, A100, Th51;
for n being object st n in NAT holds
I . n = (Partial_Sums J) . n

proof

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

proof

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

end;

E \ (union E0) = dom (G . 0) by A71;
then (Partial_Sums J) . n1 = Integral (M,((Partial_Sums G) . n1)) by A76, A100, A111, Th46;
then (Partial_Sums J) . n1 = Integral (M,(H . n1)) by A85;
then (Partial_Sums J) . n1 = Integral (M,((F . n1) | (E \ (union E0)))) by A52;
hence I . n = (Partial_Sums J) . n by A53; :: thesis:

end;

then A112: I = Partial_Sums J ;
dom (lim (Partial_Sums G)) = dom (H . 0) by A97, MESFUNC8:def 9;
then dom (lim (Partial_Sums G)) = E \ (union E0) by A56;
then A113: lim I = Integral (M,(lim H)) by A97, A110, A112;
take I ; :: thesis:
A114: 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:
A115: E \ (union E0) c= E by XBOOLE_1:36;
assume x in E \ (union E0) ; :: thesis:
hence F # x is convergent by A6, A115; :: thesis:

end;

A116: 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 A50;
hence (M * L) . n = 0 by A48; :: thesis:

end;

M * L is nonnegative by MEASURE2:1;
then SUM (M * L) = (Ser (M * L)) . 0 by A116, SUPINF_2:48;
then SUM (M * L) = (M * L) . 0 by SUPINF_2:def 11;
then SUM (M * L) = 0 by A116;
then M . (union E0) <= 0 by MEASURE2:11;
then A117: M . (union E0) = 0 by SUPINF_2:51;
A118: 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;
A119: I . n = Integral (M,((F . n1) | (E \ (union E0)))) by A53;
dom (F . n) = E by A1, A3;
hence I . n = Integral (M,(F . n)) by A4, A117, A119, MESFUNC5:95; :: thesis:

end;

for n, m being Nat st m <= n holds
I . m <= I . n

proof

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

end;

then A126: I is non-decreasing by RINFSUP2:7;
E = dom (lim F) by A1, MESFUNC8:def 9;
then A127: Integral (M,(lim F)) = Integral (M,((lim F) | (E \ (union E0)))) by A7, A117, 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 A127, A52, A118, A126, A114, A113, Th19, RINFSUP2:37; :: thesis:

end;