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,REAL st dom f = {} holds
f is_integrable_on M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st dom f = {} holds
f is_integrable_on M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st dom f = {} holds
f is_integrable_on M
let f be PartFunc of X,REAL; :: thesis: ( dom f = {} implies f is_integrable_on M )
assume A1: dom f = {} ; :: thesis: f is_integrable_on M
then dom f in S by MEASURE1:7;
then consider E0 being Element of S such that
A2: E0 = dom f ;
for r being Real holds E0 /\ (less_dom ((R_EAL f),r)) in S by A1, A2;
then R_EAL f is E0 -measurable ;
then A3: f is E0 -measurable ;
M . E0 = 0 by A1, A2, VALUED_0:def 19;
then f | E0 is_integrable_on M by A2, A3, MESFUN6C:20;
hence f is_integrable_on M by A2; :: thesis: verum