let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real ex NORM being Function of the carrier of (Pre-Lp-Space M,k),REAL st
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) & NORM . x = r to_power (1 / k) ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for k being positive Real ex NORM being Function of the carrier of (Pre-Lp-Space M,k),REAL st
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) & NORM . x = r to_power (1 / k) ) )
let M be sigma_Measure of S; :: thesis: for k being positive Real ex NORM being Function of the carrier of (Pre-Lp-Space M,k),REAL st
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) & NORM . x = r to_power (1 / k) ) )
let k be positive Real; :: thesis: ex NORM being Function of the carrier of (Pre-Lp-Space M,k),REAL st
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) & NORM . x = r to_power (1 / k) ) )
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 VSPDef6X;
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, Lm15;
r1 to_power (1 / k) in REAL ;
hence ex y being Element of REAL st S₁[x,y] by A2, EQC01; :: thesis: verum

end;

consider F being Function of the carrier of (Pre-Lp-Space M,k),REAL such that
A5: 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 A5; :: thesis: verum