let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let f be PartFunc of X,REAL; :: thesis: for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let x be Point of (L-1-Space M); :: thesis: ( f in x implies ( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) )
assume A1: f in x ; :: thesis: ( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
reconsider y = x as Point of (Pre-L-Space M) ;
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
A2: ( y = a.e-eq-class (g,M) & g in L1_Functions M ) ;
g in y by A2, Th38;
then f a.e.= g,M by A1, Th46;
hence ( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) by A1, A2, Th39, Th49; :: thesis: verum