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
A0: E = dom (F . 0 ) and
A1: F . 0 is nonnegative and
S1: F is with_the_same_dom and
A2: for n being Nat holds F . n is_measurable_on E and
A3: 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
A4: for x being Element of X st x in E holds
F # x is convergent ; :: thesis:
E0: 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 A0, S1, MESFUNC8:def 2;
then (F . 0 ) . x <= (F . n) . x by A3;
hence 0 <= (F . n) . x by A1, SUPINF_2:70; :: thesis:

end;

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

end;

E13: lim F is_measurable_on E by A4, A0, S1, A2, MESFUNC8:25;

per cases ;

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

then consider N being Nat such that
B1: M . (E /\ (eq_dom (F . N),+infty )) <> 0 ;
B0: E = dom (F . N) by A0, S1, MESFUNC8:def 2;
then reconsider EE = E /\ (eq_dom (F . N),+infty ) as Element of S by A2, MESFUNC1:37;
B2: EE c= E by XBOOLE_1:17;
then EE c= dom (F . N) by A0, S1, MESFUNC8:def 2;
then B3: EE = dom ((F . N) | EE) by RELAT_1:91;
B4: F . N is_measurable_on EE by A2, B2, MESFUNC1:34;
EE = (dom (F . N)) /\ EE by B3, RELAT_1:90;
then B5: (F . N) | EE is_measurable_on EE by B4, MESFUNC5:48;
B9: F . N is nonnegative by E0;
EE = eq_dom ((F . N) | EE),+infty

proof

now

let x be set ; :: thesis:
assume C1: x in EE ; :: thesis:
then x in eq_dom (F . N),+infty by XBOOLE_0:def 4;
then ( x in dom (F . N) & (F . N) . x = +infty ) by MESFUNC1:def 16;
then ((F . N) | EE) . x = +infty by B3, C1, FUNCT_1:70;
hence x in eq_dom ((F . N) | EE),+infty by C1, B3, MESFUNC1:def 16; :: thesis:

end;

then C2: 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 B3, MESFUNC1:def 16;
then eq_dom ((F . N) | EE),+infty c= EE by TARSKI:def 3;
hence EE = eq_dom ((F . N) | EE),+infty by C2, XBOOLE_0:def 10; :: thesis:

end;

then M . (EE /\ (eq_dom ((F . N) | EE),+infty )) <> 0 by B1;
then C0: Integral M,((F . N) | EE) = +infty by B3, B5, B9, Lem13, MESFUNC5:21;
F . N is_measurable_on E by A2;
then Integral M,((F . N) | EE) <= Integral M,((F . N) | E) by B0, E0, B2, MESFUNC5:99;
then +infty <= Integral M,(F . N) by C0, B0, RELAT_1:98;
then D1: Integral M,(F . N) = +infty by XXREAL_0:4;
deffunc H₁( Element of NAT ) -> Element of ExtREAL = Integral M,(F . $1);
consider I being Function of NAT ,ExtREAL such that
D2: for n being Element of NAT holds I . n = H₁(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
take I ; :: thesis:
D3: 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 13;
I . n = Integral M,(F . n1) by D2;
hence I . n = Integral M,(F . n) ; :: thesis:

end;

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

proof

let n, m be Element of NAT ; :: thesis:
assume E2: m <= n ; :: thesis:
E51: ( E = dom (F . m) & E = dom (F . n) & F . m is nonnegative ) by E0, S1, A0, MESFUNC8:def 2;
E52: ( F . n is_measurable_on E & F . m is_measurable_on E ) by A2;
for x being Element of X st x in E holds
(F . m) . x <= (F . n) . x by E2, A3;
then Integral M,((F . m) | E) <= Integral M,((F . n) | E) by E51, E52, Prop3;
then Integral M,(F . m) <= Integral M,((F . n) | E) by E51, RELAT_1:97;
then Integral M,(F . m) <= Integral M,(F . n) by E51, RELAT_1:97;
then I . m <= Integral M,(F . n) by D2;
hence I . m <= I . n by D2; :: thesis:

end;

then E4: I is non-decreasing by RINFSUP2:7;
then E6: ( I is convergent & lim I = sup I ) by RINFSUP2:37;
reconsider N1 = N as Element of NAT by ORDINAL1:def 13;
E7: ( I ^\ N1 is non-decreasing & sup I = sup (I ^\ N1) ) by E4, RINFSUP2:26;
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 E5, NAT_1:12;
then I . N1 <= (I ^\ N1) . k by NAT_1:def 3;
hence +infty <= (I ^\ N1) . k by D1, D3; :: thesis:

end;

then I ^\ N1 is convergent_to_+infty by RINFSUP2:32;
then lim (I ^\ N1) = +infty by LIM;
then E9: lim I = +infty by E6, E7, RINFSUP2:37;
E12: E = dom (lim F) by A0, MESFUNC8:def 10;
( lim F is nonnegative & M . (E /\ (eq_dom (lim F),+infty )) <> 0 )

proof

E10: dom (lim F) = dom (F . 0 ) by MESFUNC8:def 10;
for x being set st x in dom (lim F) holds
(lim F) . x >= 0

proof

let x be set ; :: thesis:
assume E30: x in dom (lim F) ; :: thesis:
then reconsider x1 = x as Element of X ;
E32: F # x1 is convergent by A0, E10, E30, A4;
for n being Nat holds (F # x1) . n >= 0

proof

let n be Nat; :: thesis:
( (F . n) . x1 >= (F . 0 ) . x1 & (F . 0 ) . x1 >= 0 ) by A0, A3, E10, E30, A1, SUPINF_2:70;
hence (F # x1) . n >= 0 by MESFUNC5:def 13; :: thesis:

end;

then lim (F # x1) >= 0 by E32, LIM3a;
hence (lim F) . x >= 0 by E30, MESFUNC8:def 10; :: thesis:

end;

hence lim F is nonnegative by SUPINF_2:71; :: thesis:
E14: EE c= E /\ (eq_dom (lim F),+infty )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume E40: x in EE ; :: thesis:
then E41: ( x in E & x in eq_dom (F . N),+infty ) by XBOOLE_0:def 4;
reconsider x1 = x as Element of X by E40;
( x1 in dom (F . N) & (F . N) . x1 = +infty ) by E41, MESFUNC1:def 16;
then E44: (F # x1) . N = +infty by MESFUNC5:def 13;
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 E41, A3;
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 E46: F # x1 is non-decreasing by RINFSUP2:7;
then E47: ( F # x1 is convergent & lim (F # x1) = sup (F # x1) ) by RINFSUP2:37;
E48: ( (F # x1) ^\ N1 is non-decreasing & sup (F # x1) = sup ((F # x1) ^\ N1) ) by E46, 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 E44, E48, RINFSUP2:7;
then (F # x1) ^\ N1 is convergent_to_+infty by RINFSUP2:32;
then lim ((F # x1) ^\ N1) = +infty by LIM;
then lim (F # x1) = +infty by E47, E48, RINFSUP2:37;
then (lim F) . x1 = +infty by E10, E41, A0, MESFUNC8:def 10;
then x in eq_dom (lim F),+infty by E12, E41, MESFUNC1:def 16;
hence x in E /\ (eq_dom (lim F),+infty ) by E41, XBOOLE_0:def 4; :: thesis:

end;

E16: E /\ (eq_dom (lim F),+infty ) is Element of S by E12, E13, MESFUNC1:37;
0 < M . (E /\ (eq_dom (F . N),+infty )) by B1, SUPINF_2:70;
hence M . (E /\ (eq_dom (lim F),+infty )) <> 0 by E16, E14, MEASURE1:62; :: thesis:

end;

hence ( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & Integral M,(lim F) = lim I ) by E9, E12, E13, E4, D3, Lem13, RINFSUP2:37; :: thesis:

end;

suppose F0: 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 );
F1: 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 A0, S1, MESFUNC8:def 2;
then reconsider A = E /\ (eq_dom (F . n),+infty ) as Element of S by A2, MESFUNC1:37;
take A ; :: thesis:
thus S₁[n,A] ; :: thesis:

end;

consider L being Function of NAT ,S such that
F2: for n being Element of NAT holds S₁[n,L . n] from FUNCT_2:sch 3(F1);
F3: rng L is N_Sub_set_fam of X by MEASURE1:52;
rng L c= S by RELAT_1:def 19;
then reconsider E0 = rng L as N_Measure_fam of S by F3, MEASURE2:def 1;
F5: M * L is nonnegative by MEASURE2:1;
F6: 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:23;
then (M * L) . n = M . (E /\ (eq_dom (F . n),+infty )) by F2;
hence (M * L) . n = 0 by F0; :: thesis:

end;

then SUM (M * L) = (Ser (M * L)) . 0 by F5, SUPINF_2:67;
then SUM (M * L) = (M * L) . 0 by SUPINF_2:63;
then SUM (M * L) = 0 by F6;
then F7: M . (union E0) <= 0 by MEASURE2:13;
F8: M . (union E0) = 0 by F7, SUPINF_2:70;
F9: E = dom (lim F) by A0, MESFUNC8:def 10;
set E1 = E \ (union E0);
LL1: Integral M,(lim F) = Integral M,((lim F) | (E \ (union E0))) by E13, F8, F9, MESFUNC5:101;
L4: E \ (union E0) c= E by XBOOLE_1:36;
then AA2: for n being Nat holds F . n is_measurable_on E \ (union E0) by A2, MESFUNC1:34;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (F . $1) | (E \ (union E0));
consider H being Functional_Sequence of X,ExtREAL such that
G1: for n being Nat holds H . n = H₁(n) from SEQFUNC:sch 1();
G2: 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:
G20: E \ (union E0) c= dom (F . n) by L4, A0, S1, MESFUNC8:def 2;
dom (H . n) = dom ((F . n) | (E \ (union E0))) by G1;
hence dom (H . n) = E \ (union E0) by G20, RELAT_1:91; :: thesis:
(F . n) | (E \ (union E0)) is nonnegative by E0, MESFUNC5:21;
then H . n is nonnegative by G1;
hence H . n is without-infty by MESFUNC5:18; :: thesis:
for x being set st x in dom (H . n) holds
(H . n) . x < +infty

proof

let x be set ; :: thesis:
assume x in dom (H . n) ; :: thesis:
then x in dom ((F . n) | (E \ (union E0))) by G1;
then G5: ( x in E \ (union E0) & x in dom (F . n) ) by RELAT_1:86;
(H . n) . x = ((F . n) | (E \ (union E0))) . x by G1;
then G4: (H . n) . x = (F . n) . x by G5, FUNCT_1:72;
assume (H . n) . x >= +infty ; :: thesis:
then (F . n) . x = +infty by G4, XXREAL_0:4;
then G7: x in eq_dom (F . n),+infty by G5, MESFUNC1:def 16;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
( L . n = E /\ (eq_dom (F . n1),+infty ) & dom L = NAT ) by F2, FUNCT_2:def 1;
then ( x in L . n & L . n in rng L ) by G7, G5, L4, FUNCT_1:12, XBOOLE_0:def 4;
then x in union E0 by TARSKI:def 4;
hence contradiction by G5, XBOOLE_0:def 5; :: thesis:

end;

hence H . n is without+infty by MESFUNC5:17; :: 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 G2;
hence dom (H . n) = dom (H . m) by G2; :: 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);
K1: 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
K3: ( 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(K1);
J3: 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 13;
G . (n + 1) = (H . (n1 + 1)) - (H . n) by K3;
hence G . (n + 1) = (H . (n + 1)) - (H . n) ; :: thesis:

end;

now

let f be set ; :: thesis:
assume f in rng G ; :: thesis:
then consider m being set such that
K41: ( m in dom G & f = G . m ) by FUNCT_1:def 5;
reconsider m = m as Nat by K41, K3;
defpred S₃[ Nat] means G . $1 is PartFunc of X,ExtREAL ;
K42: S₃[ 0 ] by K3;
K43: 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 J3;
hence S₃[n + 1] ; :: thesis:

end;

for n being Nat holds S₃[n] from NAT_1:sch 2(K42, K43);
then G . m is PartFunc of X,ExtREAL ;
hence f in PFuncs X,ExtREAL by K41, PARTFUN1:119; :: thesis:

end;

then rng G c= PFuncs X,ExtREAL by TARSKI:def 3;
then reconsider G = G as Functional_Sequence of X,ExtREAL by K3, FUNCT_2:def 1, RELSET_1:11;
Y1: 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
Y11: n = k + 1 by NAT_1:6;
M0: G . (k + 1) = (H . (k + 1)) - (H . k) by J3;
( H . (k + 1) is without-infty & H . (k + 1) is without+infty & H . k is without+infty & H . k is without-infty ) by G2;
then dom (G . (k + 1)) = (dom (H . (k + 1))) /\ (dom (H . k)) by M0, MESFUNC5:23;
then dom (G . (k + 1)) = (E \ (union E0)) /\ (dom (H . k)) by G2;
then dom (G . (k + 1)) = (E \ (union E0)) /\ (E \ (union E0)) by G2;
hence dom (G . n) = E \ (union E0) by Y11; :: thesis:

end;

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

end;

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

proof

let n be Nat; :: thesis:
P27: ( n = 0 implies G . n is nonnegative )

proof

assume P28: n = 0 ; :: thesis:
(F . n) | (E \ (union E0)) is nonnegative by E0, MESFUNC5:21;
hence G . n is nonnegative by P28, K3, G1; :: thesis:

end;

( n <> 0 implies G . n is nonnegative )

proof

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

proof

let x be set ; :: thesis:
assume M21: x in dom (G . (k + 1)) ; :: thesis:
M23: dom (G . (k + 1)) = E \ (union E0) by Y1;
( (H . (k + 1)) . x = ((F . (k + 1)) | (E \ (union E0))) . x & (H . k) . x = ((F . k) | (E \ (union E0))) . x ) by G1;
then M25: ( (H . (k + 1)) . x = (F . (k + 1)) . x & (H . k) . x = (F . k) . x ) by M21, M23, FUNCT_1:72;
(F . k) . x <= (F . (k + 1)) . x by A3, L4, M21, M23, NAT_1:11;
then ((H . (k + 1)) . x) - ((H . k) . x) >= 0 by M25, XXREAL_3:43;
hence 0 <= (G . (k + 1)) . x by M0, M21, MESFUNC1:def 4; :: thesis:

end;

hence G . n is nonnegative by P28, SUPINF_2:71; :: thesis:

end;

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

end;

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

proof

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

proof

let k be Nat; :: thesis:
assume P23: S₃[k] ; :: thesis:
M0: G . (k + 1) = (H . (k + 1)) - (H . k) by J3;
H . (k + 1) = (G . (k + 1)) + (H . k)

proof

M3: ( H . (k + 1) is without-infty & H . (k + 1) is without+infty & H . k is without+infty & H . k is without-infty ) by G2;
M2: dom (G . (k + 1)) = E \ (union E0) by Y1;
M6: G . (k + 1) is without-infty by Z1, MESFUNC5:18;
then dom ((G . (k + 1)) + (H . k)) = (dom (G . (k + 1))) /\ (dom (H . k)) by M3, MESFUNC5:22;
then dom ((G . (k + 1)) + (H . k)) = (E \ (union E0)) /\ (E \ (union E0)) by M2, G2;
then M1: dom (H . (k + 1)) = dom ((G . (k + 1)) + (H . k)) by G2;
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:
assume M4: x in dom (H . (k + 1)) ; :: thesis:
then M5: x in E \ (union E0) by G2;
( (H . (k + 1)) . x <> -infty & (H . (k + 1)) . x <> +infty & (H . k) . x <> -infty & (H . k) . x <> +infty & (G . (k + 1)) . x <> -infty ) by M3, M6, MESFUNC5:def 5, MESFUNC5:def 6;
then (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = ((H . (k + 1)) . x) - (((H . k) . x) - ((H . k) . x)) by XXREAL_3:33;
then (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = ((H . (k + 1)) . x) - 0. by XXREAL_3:7;
then (((H . (k + 1)) . x) - ((H . k) . x)) + ((H . k) . x) = (H . (k + 1)) . x by XXREAL_3:4;
then (H . (k + 1)) . x = ((G . (k + 1)) . x) + ((H . k) . x) by M0, M5, M2, MESFUNC1:def 4;
hence (H . (k + 1)) . x = ((G . (k + 1)) + (H . k)) . x by M4, M1, MESFUNC1:def 3; :: thesis:

end;

hence H . (k + 1) = (G . (k + 1)) + (H . k) by M1, PARTFUN1:34; :: thesis:

end;

hence S₃[k + 1] by P23, Def0; :: thesis:

end;

for k being Nat holds S₃[k] from NAT_1:sch 2(P21, P22);
then H . n = (Partial_Sums G) . n ;
hence H . n1 = (Partial_Sums G) . n1 ; :: thesis:

end;

P2: for n being Nat holds
( H . n = (Partial_Sums G) . n & lim H = lim (Partial_Sums G) ) by X0, FUNCT_2:18;
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 Y1;
hence dom (G . n) = dom (G . m) by Y1; :: thesis:

end;

then reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
reconsider G = G as with_the_same_dom additive Functional_Sequence of X,ExtREAL by Z1, LIM4;
V1: E \ (union E0) = dom (G . 0 ) by G2, K3;
T20: 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 & H . k is without+infty ) by G2;
then ( -infty < (H . k) . x & (H . k) . x < +infty ) by MESFUNC5:def 5, MESFUNC5:def 6;
hence |.((H . k) . x).| < +infty by EXTREAL2:101, XXREAL_0:4; :: thesis:

end;

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

end;

V3: 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
T2: n = k + 1 by NAT_1:6;
T21: ( H . (k + 1) is_measurable_on E \ (union E0) & H . k is_measurable_on E \ (union E0) ) by L4, A0, S1, G1, AA2, Prop1;
T22: E \ (union E0) = dom (H . k) by G2;
T23: ( H . (k + 1) is real-valued & H . k is real-valued ) by T20;
G . (k + 1) = (H . (k + 1)) - (H . k) by J3;
hence G . n is_measurable_on E \ (union E0) by T2, T23, T21, T22, MESFUNC2:13; :: thesis:

end;

hence G . n is_measurable_on E \ (union E0) by L4, A0, S1, G1, AA2, Prop1, K3; :: thesis:

end;

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 Q0: x in E \ (union E0) ; :: thesis:
E \ (union E0) c= E by XBOOLE_1:36;
then F # x is convergent by A4, Q0;
then H # x is convergent by Q0, G1, Lm16;
then (Partial_Sums G) # x is convergent by X0, FUNCT_2:18;
then Partial_Sums (G # x) is convergent by Q0, V1, Cor01;
hence G # x is summable by Def2; :: thesis:

end;

then consider J being ExtREAL_sequence such that
Q2: ( ( for n being Nat holds J . n = Integral M,((G . n) | (E \ (union E0))) ) & J is summable & Integral M,((lim (Partial_Sums G)) | (E \ (union E0))) = Sum J ) by V1, V3, Z1, Th131;
deffunc H₂( Element of NAT ) -> Element of ExtREAL = Integral M,((F . $1) | (E \ (union E0)));
consider I being Function of NAT ,ExtREAL such that
P3: for n being Element of NAT holds I . n = H₂(n) from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
take I ; :: thesis:
P4: 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 13;
P41: I . n = Integral M,((F . n1) | (E \ (union E0))) by P3;
dom (F . n) = E by A0, S1, MESFUNC8:def 2;
hence I . n = Integral M,(F . n) by A2, P41, F8, MESFUNC5:101; :: 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:
assume P51: m <= n ; :: thesis:
P52: ( dom (F . m) = E & dom (F . n) = E ) by A0, S1, MESFUNC8:def 2;
then P54: for x being Element of X st x in dom (F . m) holds
(F . m) . x <= (F . n) . x by A3, P51;
P55: ( F . m is nonnegative & F . n is nonnegative ) by E0;
( F . m is_measurable_on E & F . n is_measurable_on E ) by A2;
then integral+ M,(F . m) <= integral+ M,(F . n) by P52, P55, P54, MESFUNC5:91;
then Integral M,(F . m) <= integral+ M,(F . n) by P52, A2, P55, MESFUNC5:94;
then P56: Integral M,(F . m) <= Integral M,(F . n) by P52, A2, P55, MESFUNC5:94;
I . m <= Integral M,(F . n) by P4, P56;
hence I . m <= I . n by P4; :: thesis:

end;

then X1: I is non-decreasing by RINFSUP2:7;
R3: 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:
assume Q0: x in E \ (union E0) ; :: thesis:
E \ (union E0) c= E by XBOOLE_1:36;
hence F # x is convergent by A4, Q0; :: thesis:

end;

dom (lim (Partial_Sums G)) = dom (H . 0 ) by P2, MESFUNC8:def 10;
then R5: dom (lim (Partial_Sums G)) = E \ (union E0) by G2;
R2: E \ (union E0) c= dom (F . 0 ) by A0, XBOOLE_1:36;
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 ;
R64: for n being Nat holds J . n = Integral M,(G . n)

proof

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

end;

E \ (union E0) = dom (G . 0 ) by Y1;
then (Partial_Sums J) . n1 = Integral M,((Partial_Sums G) . n1) by V3, R64, Z1, FSUM3;
then (Partial_Sums J) . n1 = Integral M,(H . n1) by X0;
then (Partial_Sums J) . n1 = Integral M,((F . n1) | (E \ (union E0))) by G1;
hence I . n = (Partial_Sums J) . n by P3; :: thesis:

end;

then I = Partial_Sums J by FUNCT_2:18;
then lim I = Integral M,(lim H) by P2, R5, Q2, RELAT_1:97;
hence ( ( for n being Nat holds I . n = Integral M,(F . n) ) & I is convergent & Integral M,(lim F) = lim I ) by P4, X1, LL1, R2, G1, R3, Lm15, RINFSUP2:37; :: thesis:

end;