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 Def18;
then consider f being PartFunc of X,REAL such that
A2: x = a.e-eq-class (f,M) and
A3: 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 A3;
then Integral (M,(abs f)) in REAL by Th44;
hence ex y being Element of REAL st S₁[x,y] by A2, A3, Th38; :: thesis: verum

end;

consider f being Function of (Pre-L-Space M),REAL such that
A4: 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 A4; :: thesis: verum