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-CSpace M),REAL st
for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX 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-CSpace M),REAL st
for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX 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-CSpace M),REAL st
for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st
( f in x & NORM . x = Integral (M,(abs f)) )
defpred S₁[ set , set ] means ex f being PartFunc of X,COMPLEX st
( f in $1 & $2 = Integral (M,(abs f)) );
A1: for x being Point of (Pre-L-CSpace M) ex y being Element of REAL st S₁[x,y]

proof

let x be Point of (Pre-L-CSpace M); :: thesis: ex y being Element of REAL st S₁[x,y]
x in the carrier of (Pre-L-CSpace M) ;
then x in CCosetSet M by Def19;
then consider f being PartFunc of X,COMPLEX such that
A2: x = a.e-Ceq-class (f,M) and
A3: f in L1_CFunctions M ;
ex f0 being PartFunc of X,COMPLEX st
( f = f0 & ex ND being Element of S st
( M . ND = 0 & dom f0 = ND ` & f0 is_integrable_on M ) ) by A3;
then Integral (M,(abs f)) in REAL by Th37;
hence ex y being Element of REAL st S₁[x,y] by A2, A3, Th31; :: thesis: verum

end;

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