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 Ef -measurable & (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 Ef -measurable & (abs f) to_power k is_integrable_on M ) } c= PFuncs (X,REAL)
reconsider g = X --> (In (0,REAL)) as Function of X,REAL by FUNCOP_1:46;
reconsider Ef = X as Element of S by MEASURE1:34;
set h = (abs g) to_power k;
A2:
dom g = X
by FUNCOP_1:13;
for x being set st x in dom g holds
g . x = 0
by FUNCOP_1:7;
then A3:
g is Ef -measurable
by A2, LPSPACE1:52;
Ef ` = {}
by XBOOLE_1:37;
then A4:
M . (Ef `) = 0
by VALUED_0:def 19;
for x being object st x in dom (X --> 0) holds
0 <= (X --> 0) . x
;
then
abs g = X --> 0
by Th14, MESFUNC6:52;
then A5:
(abs g) to_power k = g
by Th12;
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:7;
then
(abs g) to_power k is_integrable_on M
by Th15, A5, A2;
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 Ef -measurable & (abs f) to_power k is_integrable_on M ) }
by A3, A4, A2;
hence
{ f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef `) = 0 & dom f = Ef & f is Ef -measurable & (abs f) to_power k is_integrable_on M ) } is non empty Subset of (RLSp_PFunct X)
by A1; verum