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 --> 0 as Function of X,REAL by FUNCOP_1:58;
reconsider ND = X as Element of S by MEASURE1:66;
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:13;
then A3: g is_integrable_on M by A2, Lm2;
for x being set st x in dom g holds
0 <= g . x ;
then abs g = g by Lm002b, MESFUNC6:52;
then A4: (abs g) to_power k = g by Lm001;
for x being set st x in dom g holds
g . x = 0 by FUNCOP_1:13;
then g is_measurable_on ND by A2, LPSPACE1:53;
hence ( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions M,k ) by A1, A2, A3, A4; :: thesis: verum