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 (Pre-L-Space M) = the carrier of (Pre-Lp-Space (M,1)) by Th75;

now :: thesis: for x being Element of the carrier of (Pre-L-Space M) holds (L-1-Norm M) . x = (Lp-Norm (M,1)) . x

let x be Element of the carrier of (Pre-L-Space M); :: thesis: (L-1-Norm M) . x = (Lp-Norm (M,1)) . x
x in the carrier of (Pre-L-Space M) ;
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 & (L-1-Norm M) . 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,(|.b.| to_power 1)) & (Lp-Norm (M,1)) . x = r to_power (1 / 1) ) ) by A1, Def12;
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 A6, LPSPACE1:30;
then A7: Integral (M,|.a.|) = Integral (M,|.b.|) by A2, A3, A5, LPSPACE1:45;
|.b.| to_power 1 = |.b.| by Th8;
hence (L-1-Norm M) . x = (Lp-Norm (M,1)) . x by A3, A5, A7, POWER:25; :: thesis: verum

end;

hence L-1-Norm M = Lp-Norm (M,1) by A1, FUNCT_2:63; :: thesis: verum