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 Th009;

now

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
B1: ( x = a.e-eq-class (g,M) & g in L1_Functions M ) ;
consider a being PartFunc of X,REAL such that
A4: ( a in x & (L-1-Norm M) . x = Integral (M,(abs a)) ) by LPSPACE1:def 19;
B2: 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 B1, A4;
consider b being PartFunc of X,REAL such that
A5: ( b in x & ex r being Real st
( r = Integral (M,((abs b) to_power 1)) & (Lp-Norm (M,1)) . x = r to_power (1 / 1) ) ) by A1, DefLpNORM;
B4: 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 B1, A5;
a a.e.= g,M by B2, LPSPACE1:29;
then a a.e.= b,M by B4, LPSPACE1:30;
then B6: Integral (M,(abs a)) = Integral (M,(abs b)) by B1, A4, A5, LPSPACE1:45;
(abs b) to_power 1 = abs b by LmPW006;
hence (L-1-Norm M) . x = (Lp-Norm (M,1)) . x by A4, A5, B6, POWER:30; :: thesis: verum

end;

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