let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S holds X --> 0 in L1_Functions M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds X --> 0 in L1_Functions M

let M be sigma_Measure of S; :: thesis: X --> 0 in L1_Functions M

reconsider ND = {} as Element of S by MEASURE1:34;

A1: M . ND = 0 by VALUED_0:def 19;

X --> (In (0,REAL)) is Function of X,REAL by FUNCOP_1:46;

then A2: dom (X --> 0) = ND ` by FUNCT_2:def 1;

for x being Element of X st x in dom (X --> 0) holds

(X --> 0) . x = 0 by FUNCOP_1:7;

then X --> 0 is_integrable_on M by A2, Th15;

hence X --> 0 in L1_Functions M by A1, A2; :: thesis: verum

for M being sigma_Measure of S holds X --> 0 in L1_Functions M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds X --> 0 in L1_Functions M

let M be sigma_Measure of S; :: thesis: X --> 0 in L1_Functions M

reconsider ND = {} as Element of S by MEASURE1:34;

A1: M . ND = 0 by VALUED_0:def 19;

X --> (In (0,REAL)) is Function of X,REAL by FUNCOP_1:46;

then A2: dom (X --> 0) = ND ` by FUNCT_2:def 1;

for x being Element of X st x in dom (X --> 0) holds

(X --> 0) . x = 0 by FUNCOP_1:7;

then X --> 0 is_integrable_on M by A2, Th15;

hence X --> 0 in L1_Functions M by A1, A2; :: thesis: verum