defpred S_{1}[ set , set ] means ex f being PartFunc of X,REAL st

( f in $1 & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & $2 = r to_power (1 / k) ) );

A1: for x being Point of (Pre-Lp-Space (M,k)) ex y being Element of REAL st S_{1}[x,y]

A3: for x being Point of (Pre-Lp-Space (M,k)) holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A1);

take F ; :: thesis: for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & F . x = r to_power (1 / k) ) )

thus for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & F . x = r to_power (1 / k) ) ) by A3; :: thesis: verum

( f in $1 & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & $2 = r to_power (1 / k) ) );

A1: for x being Point of (Pre-Lp-Space (M,k)) ex y being Element of REAL st S

proof

consider F being Function of the carrier of (Pre-Lp-Space (M,k)),REAL such that
let x be Point of (Pre-Lp-Space (M,k)); :: thesis: ex y being Element of REAL st S_{1}[x,y]

x in the carrier of (Pre-Lp-Space (M,k)) ;

then x in CosetSet (M,k) by Def11;

then consider f being PartFunc of X,REAL such that

A2: ( x = a.e-eq-class_Lp (f,M,k) & f in Lp_Functions (M,k) ) ;

reconsider r1 = Integral (M,((abs f) to_power k)) as Element of REAL by A2, Th49;

r1 to_power (1 / k) in REAL by XREAL_0:def 1;

hence ex y being Element of REAL st S_{1}[x,y]
by A2, Th38; :: thesis: verum

end;x in the carrier of (Pre-Lp-Space (M,k)) ;

then x in CosetSet (M,k) by Def11;

then consider f being PartFunc of X,REAL such that

A2: ( x = a.e-eq-class_Lp (f,M,k) & f in Lp_Functions (M,k) ) ;

reconsider r1 = Integral (M,((abs f) to_power k)) as Element of REAL by A2, Th49;

r1 to_power (1 / k) in REAL by XREAL_0:def 1;

hence ex y being Element of REAL st S

A3: for x being Point of (Pre-Lp-Space (M,k)) holds S

take F ; :: thesis: for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & F . x = r to_power (1 / k) ) )

thus for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & F . x = r to_power (1 / k) ) ) by A3; :: thesis: verum