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 and
A2: f is_measurable_on E and
A3: f is nonnegative and
A4: M . (E /\ (eq_dom f,+infty )) <> 0 ; :: thesis:
reconsider EE = E /\ (eq_dom f,+infty ) as Element of S by A1, A2, MESFUNC1:37;
A5: dom (f | E) = E by A1, RELAT_1:91;
E = (dom f) /\ E by A1;
then A6: f | E is_measurable_on E by A2, MESFUNC5:48;
integral+ M,(f | EE) <= integral+ M,(f | E) by A1, A2, A3, MESFUNC5:89, XBOOLE_1:17;
then A7: integral+ M,(f | EE) <= Integral M,(f | E) by A3, A6, A5, MESFUNC5:21, MESFUNC5:94;
A8: EE = (dom f) /\ EE by A1, XBOOLE_1:17, XBOOLE_1:28;
f is_measurable_on EE by A2, MESFUNC1:34, XBOOLE_1:17;
then A9: f | EE is_measurable_on EE by A8, MESFUNC5:48;
A10: f | EE is nonnegative by A3, MESFUNC5:21;
reconsider ES = {} as Element of S by PROB_1:10;
deffunc H₁( Element of NAT ) -> Element of bool [:X,ExtREAL :] = $1 (#) ((chi EE,X) | EE);
consider G being Function such that
A11: ( 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
A12: m in dom G and
A13: g = G . m by FUNCT_1:def 5;
reconsider m = m as Element of NAT by A11, A12;
g = m (#) ((chi EE,X) | EE) by A11, A13;
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 A11, FUNCT_2:def 1, RELSET_1:11;
A14: 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;
EE c= X ;
then EE c= dom (chi EE,X) by FUNCT_3:def 3;
then A15: dom ((chi EE,X) | EE) = EE by RELAT_1:91;
A16: G . n = n1 (#) ((chi EE,X) | EE) by A11;
hence A17: dom (G . n) = EE by A15, MESFUNC1:def 6; :: thesis:
let x be set ; :: thesis:
assume A18: x in dom (G . n) ; :: thesis:
then reconsider x1 = x as Element of X ;
(chi EE,X) . x1 = 1. by A17, A18, FUNCT_3:def 3;
then ((chi EE,X) | EE) . x1 = 1. by A15, A17, A18, FUNCT_1:70;
then (G . n) . x = (R_EAL n1) * 1. by A16, A18, MESFUNC1:def 6;
hence (G . n) . x = n by XXREAL_3:92; :: thesis:

end;

A19: 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 A14;
hence G . n is nonnegative by SUPINF_2:71; :: thesis:

end;

deffunc H₂( Element of NAT ) -> Element of ExtREAL = integral' M,(G . $1);
consider K being Function of NAT ,ExtREAL such that
A20: for n being Element of NAT holds K . n = H₂(n) from FUNCT_2:sch 4();
reconsider K = K as ExtREAL_sequence ;
A21: 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 A20;
hence K . n = integral' M,(G . n) ; :: thesis:

end;

A22: dom (f | EE) = EE by A1, RELAT_1:91, XBOOLE_1:17;
A23: 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 A24: n <= m ; :: thesis:
let x be Element of X; :: thesis:
assume A25: x in dom (f | EE) ; :: thesis:
then x in dom (G . n) by A22, A14;
then A26: (G . n) . x = n by A14;
x in dom (G . m) by A22, A14, A25;
hence (G . n) . x <= (G . m) . x by A14, A24, A26; :: thesis:

end;

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

proof

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

end;

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

proof

let i be Element of NAT ; :: thesis:
for x being set st x in dom (G . i) holds
(G . i) . x = R_EAL i by A14;
then integral' M,(G . i) = (R_EAL i) * (M . (dom (G . i))) by A27, MESFUNC5:77;
hence K . i = (R_EAL i) * (M . (dom (G . i))) by A21; :: thesis:

end;

M . ES <= M . EE by MEASURE1:62, XBOOLE_1:2;
then A30: 0 < M . EE by A4, VALUED_0:def 19;
A31: not rng K is bounded_above

proof

assume rng K is bounded_above ; :: thesis:
then consider UB being real number such that
B32: UB is UpperBound of rng K by XXREAL_2:def 10;
UB in REAL by XREAL_0:def 1;
then reconsider r = UB as Real ;

per cases by A30, XXREAL_0:10;

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

K . 1 = (R_EAL 1) * (M . (dom (G . 1))) by A29;
then K . 1 = (R_EAL 1) * (M . EE) by A14;
then A34: K . 1 = +infty by A33, 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 B32, XXREAL_2:def 1;
hence contradiction by A34, XXREAL_0:4; :: 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
A35: r / ee < n by SEQ_4:10;
K . n = (R_EAL n) * (M . (dom (G . n))) by A29;
then K . n = (R_EAL n) * (M . EE) by A14;
then A36: K . n = n * ee by EXTREAL1:13;
(r / ee) * ee < n * ee by A30, A35, XREAL_1:70;
then r / (ee / ee) < K . n by A36, XCMPLX_1:83;
then A37: r < K . n by A4, XCMPLX_1:51;
dom K = NAT by FUNCT_2:def 1;
then K . n in rng K by FUNCT_1:12;
then K . n <= r by B32, XXREAL_2:def 1;
hence contradiction by A37; :: thesis:

end;

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

proof

let n, m be Element of NAT ; :: thesis:
dom (G . m) = EE by A14;
then A38: K . m = (R_EAL m) * (M . EE) by A29;
dom (G . n) = EE by A14;
then A39: K . n = (R_EAL n) * (M . EE) by A29;
assume m <= n ; :: thesis:
hence K . m <= K . n by A30, A38, A39, XXREAL_3:82; :: thesis:

end;

then A40: K is non-decreasing by RINFSUP2:7;
then A41: lim K = sup K by RINFSUP2:37;
A42: 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 A43: x in dom (f | EE) ; :: thesis:
then A44: x in EE by A1, RELAT_1:91, XBOOLE_1:17;
then x in eq_dom f,+infty by XBOOLE_0:def 4;
then f . x = +infty by MESFUNC1:def 16;
then A45: (f | EE) . x = +infty by A44, FUNCT_1:72;
A46: not rng (G # x) is bounded_above

proof

assume rng (G # x) is bounded_above ; :: thesis:
then consider UB being real number such that
B47: UB is UpperBound of rng (G # x) by XXREAL_2:def 10;
UB in REAL by XREAL_0:def 1;
then reconsider r = UB as Real ;
consider n being Element of NAT such that
A48: r < n by SEQ_4:10;
x in dom (G . n) by A14, A44;
then (G . n) . x = n by A14;
then A49: UB < (G # x) . n by A48, MESFUNC5:def 13;
dom (G # x) = NAT by FUNCT_2:def 1;
then (G # x) . n in rng (G # x) by FUNCT_1:12;
hence contradiction by A49, B47, XXREAL_2:def 1; :: thesis:

end;

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 by A14;
then A50: (G . n) . x = n by A22, A14, A43;
dom (G . m) = EE by A14;
then (G . m) . x = m by A22, A14, A43;
then A51: (G # x) . m = m by MESFUNC5:def 13;
assume m <= n ; :: thesis:
hence (G # x) . m <= (G # x) . n by A50, A51, MESFUNC5:def 13; :: thesis:

end;

then A52: G # x is non-decreasing by RINFSUP2:7;
sup (rng (G # x)) is UpperBound of rng (G # x) by XXREAL_2:def 3;
then sup (G # x) = +infty by A46, XXREAL_2:53;
hence ( G # x is convergent & lim (G # x) = (f | EE) . x ) by A52, A45, RINFSUP2:37; :: thesis:

end;

sup (rng K) is UpperBound of rng K by XXREAL_2:def 3;
then A53: sup K = +infty by A31, XXREAL_2:53;
K is convergent by A40, RINFSUP2:37;
then integral+ M,(f | EE) = +infty by A10, A22, A9, A27, A19, A23, A42, A21, A41, A53, MESFUNC5:def 15;
then Integral M,(f | E) = +infty by A7, XXREAL_0:4;
hence Integral M,f = +infty by A1, RELAT_1:97; :: thesis: