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,COMPLEX
for x being Point of (L-1-CSpace M) st f in x holds
( x = a.e-Ceq-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,COMPLEX
for x being Point of (L-1-CSpace M) st f in x holds
( x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX
for x being Point of (L-1-CSpace M) st f in x holds
( x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let f be PartFunc of X,COMPLEX; :: thesis: for x being Point of (L-1-CSpace M) st f in x holds
( x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
let x be Point of (L-1-CSpace M); :: thesis: ( f in x implies ( x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) )
assume A1: f in x ; :: thesis: ( x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )
reconsider y = x as Point of (Pre-L-CSpace M) ;
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
A2: ( y = a.e-Ceq-class (g,M) & g in L1_CFunctions M ) ;
g in y by A2, Th31;
then f a.e.cpfunc= g,M by A1, Th39;
hence ( x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) by A1, A2, Th32, Th43; :: thesis: verum