let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S ex NORM being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & NORM . x = Integral M,(abs f) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S ex NORM being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & NORM . x = Integral M,(abs f) )
let M be sigma_Measure of S; :: thesis: ex NORM being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & NORM . x = Integral M,(abs f) )
defpred S₁[ set , set ] means ex f being PartFunc of X,REAL st
( f in $1 & $2 = Integral M,(abs f) );
A1: for x being Point of (Pre-L-Space M) ex y being Element of REAL st S₁[x,y]

proof

let x be Point of (Pre-L-Space M); :: thesis: ex y being Element of REAL st S₁[x,y]
x in the carrier of (Pre-L-Space M) ;
then x in CosetSet M by VSPDef6X;
then consider f being PartFunc of X,REAL such that
A2: ( x = a.e-eq-class f,M & f in L1_Functions M ) ;
ex f0 being PartFunc of X,REAL st
( f = f0 & ex ND being Element of S st
( M . ND = 0 & dom f0 = ND ` & f0 is_integrable_on M ) ) by A2;
then Integral M,(abs f) in REAL by Lm15;
hence ex y being Element of REAL st S₁[x,y] by A2, EQC01; :: thesis: verum

end;

consider f being Function of (Pre-L-Space M),REAL such that
A5: for x being Point of (Pre-L-Space M) holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & f . x = Integral M,(abs f) )
thus for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & f . x = Integral M,(abs f) ) by A5; :: thesis: verum