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 & (L-1-Norm M) . y = Integral M,(abs f) ) by Def20;
y in the carrier of (Pre-L-Space M) ;
then y in CosetSet M by VSPDef6X;
then consider g being PartFunc of X,REAL such that
A2: ( y = a.e-eq-class g,M & g in L1_Functions M ) ;
g in y by A2, EQC01;
then ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M ) by A1, Lm10;
then x = a.e-eq-class f,M by EQC02, A2;
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, Lm17; :: thesis: verum