let X be non empty set ; 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; 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; 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 S1[ 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 S1[x,y]
consider f being Function of (Pre-L-CSpace M),REAL such that
A4:
for x being Point of (Pre-L-CSpace M) holds S1[x,f . x]
from FUNCT_2:sch 3(A1);
take
f
; 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; verum