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;

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

hence
L-1-Norm M = Lp-Norm (M,1)
by A1, FUNCT_2:63; :: thesis: verumlet 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;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