defpred S₁[ 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₁[x,y]

proof

let x be Point of (Pre-Lp-Space (M,k)); :: thesis: ex y being Element of REAL st S₁[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₁[x,y] by A2, Th38; :: thesis: verum

end;

consider F being Function of the carrier of (Pre-Lp-Space (M,k)),REAL such that
A3: for x being Point of (Pre-Lp-Space (M,k)) holds S₁[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