let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
let M be sigma_Measure of S; :: thesis: for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
let x be Point of (L-1-Space M); :: thesis: ( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
reconsider y = x as Point of (Pre-L-Space M) ;
consider f being PartFunc of X,REAL such that
A1: f in y and
A2: (L-1-Norm M) . y = Integral (M,(abs f)) by Def19;
y in the carrier of (Pre-L-Space M) ;
then y in CosetSet M by Def18;
then consider g being PartFunc of X,REAL such that
A3: ( y = a.e-eq-class (g,M) & g in L1_Functions M ) ;
g in y by A3, Th38;
then f a.e.= g,M by A1, Th46;
then x = a.e-eq-class (f,M) by A1, A3, Th39;
hence ( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) ) by A1, A2, Th48; :: thesis: verum