let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let A be Element of S; :: thesis:
assume that
A1: ex E being Element of S st
( E = dom f & f is E -measurable ) and
A2: f is nonnegative and
A3: M . A = 0 ; :: thesis:
consider F0 being Functional_Sequence of X,ExtREAL, K0 being ExtREAL_sequence such that
A4: for n being Nat holds
( F0 . n is_simple_func_in S & dom (F0 . n) = dom f ) and
A5: for n being Nat holds F0 . n is nonnegative and
A6: for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F0 . n) . x <= (F0 . m) . x and
A7: for x being Element of X st x in dom f holds
( F0 # x is convergent & lim (F0 # x) = f . x ) and
for n being Nat holds K0 . n = integral' (M,(F0 . n)) and
K0 is convergent and
integral+ (M,f) = lim K0 by A1, A2, Def15;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL:] = (F0 . $1) | A;
consider FA being Functional_Sequence of X,ExtREAL such that
A8: for n being Nat holds FA . n = H₁(n) from SEQFUNC:sch 1();
consider E being Element of S such that
A9: E = dom f and
A10: f is E -measurable by A1;
set C = E /\ A;
A11: f | A is nonnegative by A2, Th15;
A12: (dom f) /\ (E /\ A) = E /\ A by A9, XBOOLE_1:17, XBOOLE_1:28;
then A13: dom (f | (E /\ A)) = E /\ A by RELAT_1:61;
then A14: dom (f | (E /\ A)) = dom (f | A) by A9, RELAT_1:61;
for x being object st x in dom (f | A) holds
(f | A) . x = (f | (E /\ A)) . x

let x be object ; :: thesis:
assume A15: x in dom (f | A) ; :: thesis:
then (f | A) . x = f . x by FUNCT_1:47;
hence (f | A) . x = (f | (E /\ A)) . x by A14, A15, FUNCT_1:47; :: thesis:

end;

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
(F0 . n) | A is nonnegative by A5, Th15;
hence FA . n is nonnegative by A8; :: thesis:

end;

deffunc H₂( Nat) -> Element of ExtREAL = integral' (M,(FA . $1));
consider KA being ExtREAL_sequence such that
A19: for n being Element of NAT holds KA . n = H₂(n) from FUNCT_2:sch 4();

end;

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
F0 . n is_simple_func_in S by A4;
then integral' (M,((F0 . n) | A)) = 0 by A3, A5, Th73;
then integral' (M,(FA . n)) = 0 by A8;
hence KA . n = 0 by A20; :: thesis:

end;

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
FA . n1 = (F0 . n1) | A by A8;
hence FA . n is_simple_func_in S by A4, Th34; :: thesis:
dom (FA . n1) = dom ((F0 . n1) | A) by A8;
then dom (FA . n) = (dom (F0 . n)) /\ A by RELAT_1:61;
hence dom (FA . n) = dom (f | A) by A9, A4, A23; :: thesis:

end;

A25: for x being Element of X st x in dom (f | A) holds
( FA # x is convergent & lim (FA # x) = (f | A) . x )

let x be Element of X; :: thesis:
assume A26: x in dom (f | A) ; :: thesis:

let n be Element of NAT ; :: thesis:
A27: dom ((F0 . n) | A) = dom (FA . n) by A8
.= dom (f | A) by A24 ;
thus (FA # x) . n = (FA . n) . x by Def13
.= ((F0 . n) | A) . x by A8
.= (F0 . n) . x by A26, A27, FUNCT_1:47
.= (F0 # x) . n by Def13 ; :: thesis:

end;

end;

A30: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | A) holds
(FA . n) . x <= (FA . m) . x

let n, m be Nat; :: thesis:
assume A31: n <= m ; :: thesis:
let x be Element of X; :: thesis:
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;
assume A32: x in dom (f | A) ; :: thesis:
then x in (dom f) /\ A by RELAT_1:61;
then A33: x in dom f by XBOOLE_0:def 4;
dom ((F0 . m) | A) = dom (FA . m) by A8;
then A34: dom ((F0 . m) | A) = dom (f | A) by A24;
(FA . m) . x = ((F0 . m) | A) . x by A8;
then A35: (FA . m) . x = (F0 . m) . x by A32, A34, FUNCT_1:47;
dom ((F0 . n) | A) = dom (FA . n) by A8;
then A36: dom ((F0 . n) | A) = dom (f | A) by A24;
(FA . n) . x = ((F0 . n) | A) . x by A8;
then (FA . n) . x = (F0 . n) . x by A32, A36, FUNCT_1:47;
hence (FA . n) . x <= (FA . m) . x by A6, A31, A33, A35; :: thesis:

end;