defpred S1[ 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 S1[x,y]
proof
let x be Point of (Pre-Lp-Space (M,k)); :: thesis: ex y being Element of REAL st S1[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 ;
r1 to_power (1 / k) in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[x,y] by ; :: 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 S1[x,F . x] from 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