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 A1: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & M . A = 0 ) ; :: thesis:
then consider E being Element of S such that
A2: ( E = dom f & f is_measurable_on E ) ;
set C = E /\ A;
A3: f is_measurable_on E /\ A by A2, MESFUNC1:34, XBOOLE_1:17;
A4: (dom f) /\ (E /\ A) = E /\ A by A2, XBOOLE_1:17, XBOOLE_1:28;
then dom (f | (E /\ A)) = E /\ A by RELAT_1:90;
then A5: dom (f | (E /\ A)) = dom (f | A) by A2, RELAT_1:90;
for x being set st x in dom (f | A) holds
(f | A) . x = (f | (E /\ A)) . x

proof

let x be set ; :: thesis:
assume A6: x in dom (f | A) ; :: thesis:
then (f | A) . x = f . x by FUNCT_1:70;
hence (f | A) . x = (f | (E /\ A)) . x by A5, A6, FUNCT_1:70; :: thesis:

end;

then f | A = f | (E /\ A) by A5, FUNCT_1:9;
then A7: f | A is_measurable_on E /\ A by A3, A4, Th48;
consider F0 being Functional_Sequence of X,ExtREAL , K0 being ExtREAL_sequence such that
A8: for n being Nat holds
( F0 . n is_simple_func_in S & dom (F0 . n) = dom f ) and
A9: for n being Nat holds F0 . n is nonnegative and
A10: 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
A11: 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) ) & K0 is convergent & integral+ M,f = lim K0 ) by A1, Def15;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (F0 . $1) | A;
consider FA being Functional_Sequence of X,ExtREAL such that
A12: for n being Nat holds FA . n = H₁(n) from SEQFUNC:sch 1();
deffunc H₂( Nat) -> Element of ExtREAL = integral' M,(FA . $1);
consider KA being ExtREAL_sequence such that
A13: for n being Element of NAT holds KA . n = H₂(n) from FUNCT_2:sch 4();

A14: now

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
hence KA . n = H₂(n) by A13; :: thesis:

end;

A15: E /\ A = dom (f | A) by A2, RELAT_1:90;
A16: f | A is nonnegative by A1, Th21;
A17: for n being Nat holds
( FA . n is_simple_func_in S & dom (FA . n) = dom (f | A) )

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
( F0 . n1 is_simple_func_in S & FA . n1 = (F0 . n1) | A ) by A8, A12;
hence FA . n is_simple_func_in S by Th40; :: thesis:
dom (FA . n1) = dom ((F0 . n1) | A) by A12;
then dom (FA . n) = (dom (F0 . n)) /\ A by RELAT_1:90;
hence dom (FA . n) = dom (f | A) by A2, A8, A15; :: thesis:

end;

A18: for n being Nat holds FA . n is nonnegative

proof

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 13;
(F0 . n) | A is nonnegative by A9, Th21;
hence FA . n is nonnegative by A12; :: thesis:

end;

A19: 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

proof

let n, m be Nat; :: thesis:
assume A20: n <= m ; :: thesis:
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
let x be Element of X; :: thesis:
assume A21: x in dom (f | A) ; :: thesis:
then x in (dom f) /\ A by RELAT_1:90;
then A22: x in dom f by XBOOLE_0:def 4;
( dom ((F0 . n) | A) = dom (FA . n) & dom ((F0 . m) | A) = dom (FA . m) ) by A12;
then A23: ( dom ((F0 . n) | A) = dom (f | A) & dom ((F0 . m) | A) = dom (f | A) ) by A17;
( (FA . n) . x = ((F0 . n) | A) . x & (FA . m) . x = ((F0 . m) | A) . x ) by A12;
then ( (FA . n) . x = (F0 . n) . x & (FA . m) . x = (F0 . m) . x ) by A21, A23, FUNCT_1:70;
hence (FA . n) . x <= (FA . m) . x by A10, A20, A22; :: thesis:

end;

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

proof

let x be Element of X; :: thesis:
assume A25: x in dom (f | A) ; :: thesis:
then x in (dom f) /\ A by RELAT_1:90;
then x in dom f by XBOOLE_0:def 4;
then A26: ( F0 # x is convergent & lim (F0 # x) = f . x ) by A11;

now

let n be Element of NAT ; :: thesis:
A27: dom ((F0 . n) | A) = dom (FA . n) by A12
.= dom (f | A) by A17 ;
thus (FA # x) . n = (FA . n) . x by Def13
.= ((F0 . n) | A) . x by A12
.= (F0 . n) . x by A25, A27, FUNCT_1:70
.= (F0 # x) . n by Def13 ; :: thesis:

end;

then FA # x = F0 # x by FUNCT_2:113;
hence ( FA # x is convergent & lim (FA # x) = (f | A) . x ) by A25, A26, FUNCT_1:70; :: thesis:

end;

for n being Nat holds KA . n = R_EAL 0

proof

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 13;
( F0 . n is_simple_func_in S & F0 . n is nonnegative ) by A8, A9;
then integral' M,((F0 . n) | A) = R_EAL 0 by A1, Th79;
then integral' M,(FA . n) = R_EAL 0 by A12;
hence KA . n = R_EAL 0 by A14; :: thesis:

end;

then ( KA is convergent & lim KA = R_EAL 0 ) by Th66;
hence integral+ M,(f | A) = 0 by A7, A14, A15, A16, A17, A18, A19, A24, Def15; :: thesis: