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

for M being sigma_Measure of S

for k being positive Real holds

( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being positive Real holds

( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

let M be sigma_Measure of S; :: thesis: for k being positive Real holds

( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

let k be positive Real; :: thesis: ( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

reconsider g = X --> (In (0,REAL)) as Function of X,REAL by FUNCOP_1:46;

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

ND ` = {} by XBOOLE_1:37;

then A1: M . (ND `) = 0 by VALUED_0:def 19;

A2: dom g = X 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 A3: g is_integrable_on M by A2, Th15;

for x being object st x in dom g holds

0 <= g . x ;

then abs g = g by Th14, MESFUNC6:52;

then A4: (abs g) to_power k = g by Th12;

for x being set st x in dom g holds

g . x = 0 by FUNCOP_1:7;

then g is ND -measurable by A2, LPSPACE1:52;

hence ( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) ) by A1, A2, A3, A4; :: thesis: verum

for M being sigma_Measure of S

for k being positive Real holds

( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being positive Real holds

( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

let M be sigma_Measure of S; :: thesis: for k being positive Real holds

( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

let k be positive Real; :: thesis: ( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) )

reconsider g = X --> (In (0,REAL)) as Function of X,REAL by FUNCOP_1:46;

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

ND ` = {} by XBOOLE_1:37;

then A1: M . (ND `) = 0 by VALUED_0:def 19;

A2: dom g = X 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 A3: g is_integrable_on M by A2, Th15;

for x being object st x in dom g holds

0 <= g . x ;

then abs g = g by Th14, MESFUNC6:52;

then A4: (abs g) to_power k = g by Th12;

for x being set st x in dom g holds

g . x = 0 by FUNCOP_1:7;

then g is ND -measurable by A2, LPSPACE1:52;

hence ( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) ) by A1, A2, A3, A4; :: thesis: verum