let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds
integral+ (M,(f | A)) = 0
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds
integral+ (M,(f | A)) = 0
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds
integral+ (M,(f | A)) = 0
let f be PartFunc of X,ExtREAL; for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds
integral+ (M,(f | A)) = 0
let A be Element of S; ( ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 implies integral+ (M,(f | A)) = 0 )
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
; integral+ (M,(f | A)) = 0
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 H1( 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 = H1(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
then A16:
f | A = f | (E /\ A)
by A9, A13, FUNCT_1:2, RELAT_1:61;
f is E /\ A -measurable
by A10, MESFUNC1:30, XBOOLE_1:17;
then A17:
f | A is E /\ A -measurable
by A12, A16, Th42;
A18:
for n being Nat holds FA . n is nonnegative
deffunc H2( 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 = H2(n)
from FUNCT_2:sch 4();
A20:
now for n being Nat holds KA . n = H2(n)end;
A21:
for n being Nat holds KA . n = 0
then A22:
lim KA = 0
by Th60;
A23:
E /\ A = dom (f | A)
by A9, RELAT_1:61;
A24:
for n being Nat holds
( FA . n is_simple_func_in S & dom (FA . n) = dom (f | A) )
A25:
for x being Element of X st x in dom (f | A) holds
( FA # x is convergent & lim (FA # x) = (f | A) . x )
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
KA is convergent
by A21, Th60;
hence
integral+ (M,(f | A)) = 0
by A17, A20, A23, A11, A24, A18, A30, A25, A22, Def15; verum