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

let x be set ; :: 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_measurable_on E ) ) by A1, Lem00;
then A3: x = a.e-eq-class_Lp g,M,1 by A1, Lem03;
(abs g) to_power 1 = abs g by LmPW006;
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 by TARSKI:def 3;

now

let x be set ; :: 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_measurable_on E ) by A5, EQC00a;
A7: x = a.e-eq-class g,M by A5, A6, Lem03;
reconsider D = E ` as Element of S by MEASURE1:66;
A8: ( M . D = 0 & dom g = D ` ) by A6;
(abs g) to_power 1 is_integrable_on M by A5, Lem00a;
then abs g is_integrable_on M by LmPW006;
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 by TARSKI:def 3;
hence CosetSet M = CosetSet M,1 by A4, XBOOLE_0:def 10; :: thesis: verum