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
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,ExtREAL st dom f = {} holds
f is_integrable_on M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st dom f = {} holds
f is_integrable_on M
let f be PartFunc of X,ExtREAL; :: thesis: ( dom f = {} implies f is_integrable_on M )
assume A1: dom f = {} ; :: thesis: f is_integrable_on M
set f0 = (dom f) --> 0;
( dom ((dom f) --> 0) c= X & rng ((dom f) --> 0) c= REAL ) ;
then reconsider f0 = (dom f) --> 0 as PartFunc of X,REAL by RELSET_1:4;
dom (R_EAL f0) = dom f0 by MESFUNC5:def 7;
then A2: R_EAL f0 = f by A1;
dom f0 = dom f ;
then f0 is_integrable_on M by A1, Th1;
hence f is_integrable_on M by A2; :: thesis: verum