let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st dom f = {} holds
Integral (M,f) = 0
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st dom f = {} holds
Integral (M,f) = 0
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st dom f = {} holds
Integral (M,f) = 0
let f be PartFunc of X,ExtREAL; :: thesis: ( dom f = {} implies Integral (M,f) = 0 )
assume A1: dom f = {} ; :: thesis: Integral (M,f) = 0
then reconsider E = dom f as Element of S by MEASURE1:7;
A2: ( E = dom (max+ f) & E = dom (max- f) ) by MESFUNC2:def 2, MESFUNC2:def 3;
A3: M . E = 0 by A1, VALUED_0:def 19;
( max+ f is E -measurable & max- f is E -measurable ) by A1;
then A4: ( integral+ (M,((max+ f) | E)) = 0 & integral+ (M,((max- f) | E)) = 0 ) by A2, A3, MESFUNC5:82, MESFUN11:5;
then Integral (M,f) = (integral+ (M,(max+ f))) - 0 by A2, MESFUNC5:def 16;
hence Integral (M,f) = 0 by A2, A4, XXREAL_3:15; :: thesis: verum