set V = { f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } ;
A1: { f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } c= PFuncs X,REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } or x in PFuncs X,REAL )
assume x in { f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } ; :: thesis: x in PFuncs X,REAL
then ex f being PartFunc of X,REAL st
( x = f & ex Ef being Element of S st
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) ) ;
hence x in PFuncs X,REAL by PARTFUN1:119; :: thesis: verum

end;

reconsider g = X --> 0 as Function of X,REAL by FUNCOP_1:58;
reconsider Ef = X as Element of S by MEASURE1:66;
set h = (abs g) to_power k;
A3: dom g = X by FUNCOP_1:19;
for x being set st x in dom g holds
g . x = 0 by FUNCOP_1:13;
then A4: g is_measurable_on Ef by A3, LPSPACE1:53;
Ef ` = {} by XBOOLE_1:37;
then A6: M . (Ef ` ) = 0 by VALUED_0:def 19;
for x being set st x in dom (X --> 0 ) holds
0 <= (X --> 0 ) . x ;
then abs g = X --> 0 by Lm002b, MESFUNC6:52;
then A7: (abs g) to_power k = g by Lm001;
then for x being Element of X st x in dom ((abs g) to_power k) holds
((abs g) to_power k) . x = 0 by FUNCOP_1:13;
then (abs g) to_power k is_integrable_on M by Lm2, A7, A3;
then g in { f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } by A4, A6, A3;
hence { f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef ` ) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } is non empty Subset of (RLSp_PFunct X) by A1; :: thesis: verum