let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S holds CosetSet M = CosetSet (M,1)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds CosetSet M = CosetSet (M,1)

let M be sigma_Measure of S; :: thesis: CosetSet M = CosetSet (M,1)

hence CosetSet M = CosetSet (M,1) by A4; :: thesis: verum

for M being sigma_Measure of S holds CosetSet M = CosetSet (M,1)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds CosetSet M = CosetSet (M,1)

let M be sigma_Measure of S; :: thesis: CosetSet M = CosetSet (M,1)

now :: thesis: for x being object st x in CosetSet M holds

x in CosetSet (M,1)

then A4:
CosetSet M c= CosetSet (M,1)
;x in CosetSet (M,1)

let x be object ; :: thesis: ( x in CosetSet M implies x in CosetSet (M,1) )

assume x in CosetSet M ; :: thesis: x in CosetSet (M,1)

then consider g being PartFunc of X,REAL such that

A1: ( x = a.e-eq-class (g,M) & g in L1_Functions M ) ;

A2: ( g is_integrable_on M & ex E being Element of S st

( M . (E `) = 0 & E = dom g & g is E -measurable ) ) by A1, Lm8;

then A3: x = a.e-eq-class_Lp (g,M,1) by A1, Lm12;

(abs g) to_power 1 = abs g by Th8;

then (abs g) to_power 1 is_integrable_on M by A2, MESFUNC6:94;

then g in Lp_Functions (M,1) by A2;

hence x in CosetSet (M,1) by A3; :: thesis: verum

end;assume x in CosetSet M ; :: thesis: x in CosetSet (M,1)

then consider g being PartFunc of X,REAL such that

A1: ( x = a.e-eq-class (g,M) & g in L1_Functions M ) ;

A2: ( g is_integrable_on M & ex E being Element of S st

( M . (E `) = 0 & E = dom g & g is E -measurable ) ) by A1, Lm8;

then A3: x = a.e-eq-class_Lp (g,M,1) by A1, Lm12;

(abs g) to_power 1 = abs g by Th8;

then (abs g) to_power 1 is_integrable_on M by A2, MESFUNC6:94;

then g in Lp_Functions (M,1) by A2;

hence x in CosetSet (M,1) by A3; :: thesis: verum

now :: thesis: for x being object st x in CosetSet (M,1) holds

x in CosetSet M

then
CosetSet (M,1) c= CosetSet M
;x in CosetSet M

let x be object ; :: thesis: ( x in CosetSet (M,1) implies x in CosetSet M )

assume x in CosetSet (M,1) ; :: thesis: x in CosetSet M

then consider g being PartFunc of X,REAL such that

A5: ( x = a.e-eq-class_Lp (g,M,1) & g in Lp_Functions (M,1) ) ;

consider E being Element of S such that

A6: ( M . (E `) = 0 & dom g = E & g is E -measurable ) by A5, Th35;

A7: x = a.e-eq-class (g,M) by A5, A6, Lm12;

reconsider D = E ` as Element of S by MEASURE1:34;

A8: ( M . D = 0 & dom g = D ` ) by A6;

(abs g) to_power 1 is_integrable_on M by A5, Lm9;

then abs g is_integrable_on M by Th8;

then g is_integrable_on M by A6, MESFUNC6:94;

then g in L1_Functions M by A8;

hence x in CosetSet M by A7; :: thesis: verum

end;assume x in CosetSet (M,1) ; :: thesis: x in CosetSet M

then consider g being PartFunc of X,REAL such that

A5: ( x = a.e-eq-class_Lp (g,M,1) & g in Lp_Functions (M,1) ) ;

consider E being Element of S such that

A6: ( M . (E `) = 0 & dom g = E & g is E -measurable ) by A5, Th35;

A7: x = a.e-eq-class (g,M) by A5, A6, Lm12;

reconsider D = E ` as Element of S by MEASURE1:34;

A8: ( M . D = 0 & dom g = D ` ) by A6;

(abs g) to_power 1 is_integrable_on M by A5, Lm9;

then abs g is_integrable_on M by Th8;

then g is_integrable_on M by A6, MESFUNC6:94;

then g in L1_Functions M by A8;

hence x in CosetSet M by A7; :: thesis: verum

hence CosetSet M = CosetSet (M,1) by A4; :: thesis: verum