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 E -measurable 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:33;
A5: dom (f | E) = E by A1;
E = (dom f) /\ E by A1;
then A6: f | E is E -measurable by A2, MESFUNC5:42;
integral+ (M,(f | EE)) <= integral+ (M,(f | E)) by A1, A2, A3, MESFUNC5:83, XBOOLE_1:17;
then A7: integral+ (M,(f | EE)) <= Integral (M,(f | E)) by A3, A6, A5, MESFUNC5:15, MESFUNC5:88;
A8: EE = (dom f) /\ EE by A1, XBOOLE_1:17, XBOOLE_1:28;
f is EE -measurable by A2, MESFUNC1:30, XBOOLE_1:17;
then A9: f | EE is EE -measurable by A8, MESFUNC5:42;
A10: f | EE is nonnegative by A3, MESFUNC5:15;
reconsider ES = {} as Element of S by PROB_1:4;
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 :: thesis:

let g be object ; :: thesis:
assume g in rng G ; :: thesis:
then consider m being object such that
A12: m in dom G and
A13: g = G . m by FUNCT_1:def 3;
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:45; :: thesis:

end;

then rng G c= PFuncs (X,ExtREAL) ;
then reconsider G = G as Functional_Sequence of X,ExtREAL by A11, FUNCT_2:def 1, RELSET_1:4;
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 12;
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:62;
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:47;
then (G . n) . x = n1 * 1. by A16, A18, MESFUNC1:def 6;
hence (G . n) . x = n by XXREAL_3:81; :: thesis:

end;

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

proof

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

end;

deffunc H₂( Element of NAT ) -> Element of ExtREAL = integral' (M,(G . $1));
consider K being sequence of 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 12;
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:62, 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 12;
thus A28: dom (G . n) = dom (f | EE) by A22, A14; :: thesis:
for x being object 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 = i * (M . (dom (G . i)))

proof

let i be Element of NAT ; :: thesis:
reconsider ii = i as R_eal by XXREAL_0:def 1;
for x being object st x in dom (G . i) holds
(G . ii) . x = ii by A14;
then integral' (M,(G . i)) = ii * (M . (dom (G . ii))) by A27, MESFUNC5:71;
hence K . i = i * (M . (dom (G . i))) by A21; :: thesis:

end;

M . ES <= M . EE by MEASURE1:31, XBOOLE_1:2;
then A30: In (0,REAL) < 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 such that
A32: UB is UpperBound of rng K by XXREAL_2:def 10;
reconsider r = UB as Real ;

per cases by A30, XXREAL_0:10;

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

K . 1 = 1 * (M . (dom (G . 1))) by A29;
then K . 1 = 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:3;
then K . 1 <= UB by A32, 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 ;
consider n being Nat such that
A35: r / ee < n by SEQ_4:3;
A36: n in NAT by ORDINAL1:def 12;
K . n = n * (M . (dom (G . n))) by A29, A36;
then K . n = n * (M . EE) by A14;
then A37: K . n = n * ee by EXTREAL1:1;
(r / ee) * ee < n * ee by A30, A35, XREAL_1:68;
then r / (ee / ee) < K . n by A37, XCMPLX_1:82;
then A38: 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:3, A36;
then K . n <= r by A32, XXREAL_2:def 1;
hence contradiction by A38; :: thesis:

end;

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

proof

let n, m be Nat; :: thesis:
A39: n in NAT by ORDINAL1:def 12;
A40: m in NAT by ORDINAL1:def 12;
dom (G . m) = EE by A14;
then A41: K . m = m * (M . EE) by A29, A40;
dom (G . n) = EE by A14;
then A42: K . n = n * (M . EE) by A29, A39;
assume m <= n ; :: thesis:
hence K . m <= K . n by A30, A41, A42, XXREAL_3:71; :: thesis:

end;

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

proof

assume rng (G # x) is bounded_above ; :: thesis:
then consider UB being Real such that
A50: UB is UpperBound of rng (G # x) by XXREAL_2:def 10;
reconsider r = UB as Real ;
consider n being Nat such that
A51: r < n by SEQ_4:3;
x in dom (G . n) by A14, A47;
then (G . n) . x = n by A14;
then A52: UB < (G # x) . n by A51, MESFUNC5:def 13;
A53: n in NAT by ORDINAL1:def 12;
dom (G # x) = NAT by FUNCT_2:def 1;
then (G # x) . n in rng (G # x) by FUNCT_1:3, A53;
hence contradiction by A52, A50, XXREAL_2:def 1; :: thesis:

end;

for n, m being Nat st m <= n holds
(G # x) . m <= (G # x) . n

proof

let n, m be Nat; :: thesis:
dom (G . n) = EE by A14;
then A54: (G . n) . x = n by A22, A14, A46;
dom (G . m) = EE by A14;
then (G . m) . x = m by A22, A14, A46;
then A55: (G # x) . m = m by MESFUNC5:def 13;
assume m <= n ; :: thesis:
hence (G # x) . m <= (G # x) . n by A54, A55, MESFUNC5:def 13; :: thesis:

end;

then A56: 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 A49, XXREAL_2:53;
hence ( G # x is convergent & lim (G # x) = (f | EE) . x ) by A56, A48, RINFSUP2:37; :: thesis:

end;

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