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)

now :: thesis: for x being object st x in CosetSet M holds
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;

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

now :: thesis: for x being object st x in CosetSet (M,1) holds
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;

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