let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds L-1-Norm M = Lp-Norm (M,1)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds L-1-Norm M = Lp-Norm (M,1)
let M be sigma_Measure of S; :: thesis: L-1-Norm M = Lp-Norm (M,1)
A1: the carrier of () = the carrier of (Pre-Lp-Space (M,1)) by Th75;
now :: thesis: for x being Element of the carrier of () holds () . x = (Lp-Norm (M,1)) . x
let x be Element of the carrier of (); :: thesis: () . x = (Lp-Norm (M,1)) . x
x in the carrier of () ;
then x in CosetSet M by LPSPACE1:def 18;
then consider g being PartFunc of X,REAL such that
A2: ( x = a.e-eq-class (g,M) & g in L1_Functions M ) ;
consider a being PartFunc of X,REAL such that
A3: ( a in x & () . x = Integral (M,|.a.|) ) by LPSPACE1:def 19;
A4: ex p being PartFunc of X,REAL st
( a = p & p in L1_Functions M & g in L1_Functions M & g a.e.= p,M ) by A2, A3;
consider b being PartFunc of X,REAL such that
A5: ( b in x & ex r being Real st
( r = Integral (M,()) & (Lp-Norm (M,1)) . x = r to_power (1 / 1) ) ) by ;
A6: ex q being PartFunc of X,REAL st
( b = q & q in L1_Functions M & g in L1_Functions M & g a.e.= q,M ) by A2, A5;
a a.e.= g,M by A4;
then a a.e.= b,M by ;
then A7: Integral (M,|.a.|) = Integral (M,|.b.|) by ;
|.b.| to_power 1 = |.b.| by Th8;
hence (L-1-Norm M) . x = (Lp-Norm (M,1)) . x by ; :: thesis: verum
end;
hence L-1-Norm M = Lp-Norm (M,1) by ; :: thesis: verum