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 PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: ( E = dom f & f is_measurable_on E & f is nonnegative ) and
A2: M . (E /\ (eq_dom f,+infty )) <> 0 ; :: thesis:
reconsider EE = E /\ (eq_dom f,+infty ) as Element of S by A1, MESFUNC1:37;
A3: ( f | EE is nonnegative & f | E is nonnegative ) by A1, MESFUNC5:21;
E = (dom f) /\ E by A1;
then A4: f | E is_measurable_on E by A1, MESFUNC5:48;
A5: dom (f | E) = E by A1, RELAT_1:91;
integral+ M,(f | EE) <= integral+ M,(f | E) by A1, MESFUNC5:89, XBOOLE_1:17;
then A6: integral+ M,(f | EE) <= Integral M,(f | E) by A1, A4, A5, MESFUNC5:21, MESFUNC5:94;
A8: f is_measurable_on EE by A1, MESFUNC1:34, XBOOLE_1:17;
A9: dom (f | EE) = EE by A1, RELAT_1:91, XBOOLE_1:17;
EE = (dom f) /\ EE by A1, XBOOLE_1:17, XBOOLE_1:28;
then A10: f | EE is_measurable_on EE by A8, MESFUNC5:48;
deffunc H₁( Element of NAT ) -> Element of bool [:X,ExtREAL :] = $1 (#) ((chi EE,X) | EE);
consider G being Function such that
B1: ( dom G = NAT & ( for n being Element of NAT holds G . n = H₁(n) ) ) from FUNCT_1:sch 4();

now

let g be set ; :: thesis:
assume g in rng G ; :: thesis:
then consider m being set such that
B2: ( m in dom G & g = G . m ) by FUNCT_1:def 5;
reconsider m = m as Element of NAT by B1, B2;
g = m (#) ((chi EE,X) | EE) by B1, B2;
hence g in PFuncs X,ExtREAL by 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 B1, FUNCT_2:def 1, RELSET_1:11;
B8: for n being Nat holds
( dom (G . n) = EE & ( for x being set st x in dom (G . n) holds
(G . n) . x = n ) )

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
B3: G . n = n1 (#) ((chi EE,X) | EE) by B1;
EE c= X ;
then EE c= dom (chi EE,X) by FUNCT_3:def 3;
then B6: dom ((chi EE,X) | EE) = EE by RELAT_1:91;
hence B4: dom (G . n) = EE by B3, MESFUNC1:def 6; :: thesis:
let x be set ; :: thesis:
assume B5: x in dom (G . n) ; :: thesis:
then reconsider x1 = x as Element of X ;
(chi EE,X) . x1 = 1. by B4, B5, FUNCT_3:def 3;
then ((chi EE,X) | EE) . x1 = 1. by B5, B4, B6, FUNCT_1:70;
then (G . n) . x = (R_EAL n1) * 1. by B3, B5, MESFUNC1:def 6;
hence (G . n) . x = n by XXREAL_3:92; :: thesis:

end;

C1: for n being Nat holds
( dom (G . n) = dom (f | EE) & G . n is_simple_func_in S )

proof

let n be Nat; :: thesis:
thus C2: dom (G . n) = dom (f | EE) by A9, B8; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
for x being set st x in dom (G . n) holds
(G . n) . x = n1 by B8;
hence G . n is_simple_func_in S by C2, A9, MESFUNC6:2; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
for x being set st x in dom (G . n) holds
0 <= (G . n) . x by B8;
hence G . n is nonnegative by SUPINF_2:71; :: thesis:

end;

D1: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | EE) holds
(G . n) . x <= (G . m) . x

proof

let n, m be Nat; :: thesis:
assume D3: n <= m ; :: thesis:
let x be Element of X; :: thesis:
assume x in dom (f | EE) ; :: thesis:
then ( x in dom (G . n) & x in dom (G . m) ) by B8, A9;
then ( (G . n) . x = n & (G . m) . x = m ) by B8;
hence (G . n) . x <= (G . m) . x by D3; :: thesis:

end;

E1: for x being Element of X st x in dom (f | EE) holds
( G # x is convergent & lim (G # x) = (f | EE) . x )

proof

let x be Element of X; :: thesis:
assume E2: x in dom (f | EE) ; :: thesis:
then E3: x in EE by A1, RELAT_1:91, XBOOLE_1:17;
for n, m being Element of NAT st m <= n holds
(G # x) . m <= (G # x) . n

proof

let n, m be Element of NAT ; :: thesis:
( dom (G . n) = EE & dom (G . m) = EE ) by B8;
then ( (G . m) . x = m & (G . n) . x = n ) by A9, E2, B8;
then E4: ( (G # x) . m = m & (G # x) . n = n ) by MESFUNC5:def 13;
assume m <= n ; :: thesis:
hence (G # x) . m <= (G # x) . n by E4; :: thesis:

end;

then E5: G # x is non-decreasing by RINFSUP2:7;
E6: not rng (G # x) is bounded_above

proof

assume rng (G # x) is bounded_above ; :: thesis:
then consider UB being UpperBound of rng (G # x) such that
E61: UB in REAL by SUPINF_1:def 11;
reconsider r = UB as Real by E61;
consider n being Element of NAT such that
E62: r < n by SEQ_4:10;
dom (G # x) = NAT by FUNCT_2:def 1;
then E63: (G # x) . n in rng (G # x) by FUNCT_1:12;
x in dom (G . n) by B8, E3;
then (G . n) . x = n by B8;
then UB < (G # x) . n by E62, MESFUNC5:def 13;
hence contradiction by E63, XXREAL_2:def 1; :: thesis:

end;

sup (rng (G # x)) is UpperBound of rng (G # x) by XXREAL_2:def 3;
then E7: sup (G # x) = +infty by E6, XXREAL_2:53;
x in eq_dom f,+infty by E3, XBOOLE_0:def 4;
then ( x in dom f & f . x = +infty ) by MESFUNC1:def 16;
then (f | EE) . x = +infty by E3, FUNCT_1:72;
hence ( G # x is convergent & lim (G # x) = (f | EE) . x ) by E5, E7, RINFSUP2:37; :: thesis:

end;

deffunc H₂( Element of NAT ) -> Element of ExtREAL = integral' M,(G . $1);
consider K being Function of NAT ,ExtREAL such that
F0: for n being Element of NAT holds K . n = H₂(n) from FUNCT_2:sch 4();
reconsider K = K as ExtREAL_sequence ;
F1: for n being Nat holds K . n = integral' M,(G . n)

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
K . n = integral' M,(G . n1) by F0;
hence K . n = integral' M,(G . n) ; :: thesis:

end;

G2: for i being Element of NAT holds K . i = (R_EAL i) * (M . (dom (G . i)))

proof

let i be Element of NAT ; :: thesis:
G4: G . i is_simple_func_in S by C1;
for x being set st x in dom (G . i) holds
(G . i) . x = R_EAL i by B8;
then integral' M,(G . i) = (R_EAL i) * (M . (dom (G . i))) by G4, MESFUNC5:77;
hence K . i = (R_EAL i) * (M . (dom (G . i))) by F1; :: thesis:

end;

reconsider ES = {} as Element of S by PROB_1:42;
M . ES <= M . EE by MEASURE1:62, XBOOLE_1:2;
then L1: 0 < M . EE by A2, VALUED_0:def 19;
for n, m being Element of NAT st m <= n holds
K . m <= K . n

proof

let n, m be Element of NAT ; :: thesis:
assume G5: m <= n ; :: thesis:
( dom (G . m) = EE & dom (G . n) = EE ) by B8;
then ( K . m = (R_EAL m) * (M . EE) & K . n = (R_EAL n) * (M . EE) ) by G2;
hence K . m <= K . n by G5, L1, XXREAL_3:82; :: thesis:

end;

then K is non-decreasing by RINFSUP2:7;
then G1: ( K is convergent & lim K = sup K ) by RINFSUP2:37;
G7: not rng K is bounded_above

proof

assume rng K is bounded_above ; :: thesis:
then consider UB being UpperBound of rng K such that
G71: UB in REAL by SUPINF_1:def 11;
reconsider r = UB as Real by G71;

per cases by L1, XXREAL_0:10;

suppose G73: M . EE = +infty ; :: thesis:

K . 1 = (R_EAL 1) * (M . (dom (G . 1))) by G2;
then K . 1 = (R_EAL 1) * (M . EE) by B8;
then G74: K . 1 = +infty by G73, XXREAL_3:def 5;
dom K = NAT by FUNCT_2:def 1;
then K . 1 in rng K by FUNCT_1:12;
then K . 1 <= UB by XXREAL_2:def 1;
then UB = +infty by G74, XXREAL_0:4;
hence contradiction by G71; :: thesis:

end;

suppose M . EE in REAL ; :: thesis:

then reconsider ee = M . EE as Real ;
reconsider UB = UB as R_eal by XXREAL_0:def 1;
consider n being Element of NAT such that
G75: r / ee < n by SEQ_4:10;
dom K = NAT by FUNCT_2:def 1;
then G77: K . n in rng K by FUNCT_1:12;
K . n = (R_EAL n) * (M . (dom (G . n))) by G2;
then K . n = (R_EAL n) * (M . EE) by B8;
then G76: K . n = n * ee by EXTREAL1:13;
(r / ee) * ee < n * ee by L1, G75, XREAL_1:70;
then r / (ee / ee) < K . n by G76, XCMPLX_1:83;
then r < K . n by A2, XCMPLX_1:51;
hence contradiction by G77, XXREAL_2:def 1; :: thesis:

end;

sup (rng K) is UpperBound of rng K by XXREAL_2:def 3;
then sup K = +infty by G7, XXREAL_2:53;
then integral+ M,(f | EE) = +infty by A3, A9, A10, C1, D1, E1, F1, G1, H1, MESFUNC5:def 15;
then Integral M,(f | E) = +infty by A6, XXREAL_0:4;
hence Integral M,f = +infty by A1, RELAT_1:97; :: thesis: