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 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; :: thesis: verum

( 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)

proof

reconsider g = X --> (In (0,REAL)) as Function of X,REAL by FUNCOP_1:46;
let x be object ; :: 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 Ef -measurable & (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 Ef -measurable & (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 Ef -measurable & (abs f) to_power k is_integrable_on M ) ) ;

hence x in PFuncs (X,REAL) by PARTFUN1:45; :: thesis: verum

end;( M . (Ef `) = 0 & dom f = Ef & f is Ef -measurable & (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 Ef -measurable & (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 Ef -measurable & (abs f) to_power k is_integrable_on M ) ) ;

hence x in PFuncs (X,REAL) by PARTFUN1:45; :: thesis: verum

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; :: thesis: verum