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-CSpace M) holds
( ex f being PartFunc of X,COMPLEX st
( f in L1_CFunctions M & x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,COMPLEX 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-CSpace M) holds
( ex f being PartFunc of X,COMPLEX st
( f in L1_CFunctions M & x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,COMPLEX 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-CSpace M) holds
( ex f being PartFunc of X,COMPLEX st
( f in L1_CFunctions M & x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,COMPLEX st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
let x be Point of (L-1-CSpace M); :: thesis: ( ex f being PartFunc of X,COMPLEX st
( f in L1_CFunctions M & x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,COMPLEX st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
reconsider y = x as Point of (Pre-L-CSpace M) ;
consider f being PartFunc of X,COMPLEX such that
A1: f in y and
A2: (L-1-CNorm M) . y = Integral (M,(abs f)) by Def20;
y in the carrier of (Pre-L-CSpace M) ;
then y in CCosetSet M by Def19;
then consider g being PartFunc of X,COMPLEX such that
A3: ( y = a.e-Ceq-class (g,M) & g in L1_CFunctions M ) ;
g in y by A3, Th31;
then f a.e.cpfunc= g,M by A1, Th39;
then x = a.e-Ceq-class (f,M) by A1, A3, Th32;
hence ( ex f being PartFunc of X,COMPLEX st
( f in L1_CFunctions M & x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,COMPLEX st f in x holds
Integral (M,(abs f)) = ||.x.|| ) ) by A1, A2, Th42; :: thesis: verum