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));
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 A2, Th49;
r1 to_power (1 / k) in REAL
by XREAL_0:def 1;
hence
ex
y being
Element of
REAL st
S1[
x,
y]
by A2, Th38;
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 FUNCT_2:sch 3(A1);
take
F
; 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; verum