let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
let M be sigma_Measure of S; :: thesis: ( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )
reconsider g = X --> (In (0,REAL)) as Function of X,REAL by FUNCOP_1:46;
reconsider ND = {} as Element of S by MEASURE1:34;
A1: dom g = ND ` by FUNCT_2:def 1;
for x being Element of X st x in dom g holds
g . x = 0 by FUNCOP_1:7;
then ( M . ND = 0 & g is_integrable_on M ) by A1, Lm2, VALUED_0:def 19;
hence ( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M ) by A1; :: thesis: verum