let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds lmultCoset M = lmultCoset M,1
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds lmultCoset M = lmultCoset M,1
let M be sigma_Measure of S; :: thesis: lmultCoset M = lmultCoset M,1
A1: CosetSet M = CosetSet M,1 by Th9a;

now

let z be Element of REAL ; :: thesis: for A being Element of CosetSet M holds (lmultCoset M) . z,A = (lmultCoset M,1) . z,A
let A be Element of CosetSet M; :: thesis: (lmultCoset M) . z,A = (lmultCoset M,1) . z,A
A in { (a.e-eq-class f,M) where f is PartFunc of X,REAL : f in L1_Functions M } ;
then consider a being PartFunc of X,REAL such that
A2: ( A = a.e-eq-class a,M & a in L1_Functions M ) ;
A3: A is Element of CosetSet M,1 by Th9a;
A4: a in A by A2, LPSPACE1:38;
then A5: (lmultCoset M) . z,A = a.e-eq-class (z (#) a),M by LPSPACE1:def 17;
z (#) a in L1_Functions M by A2, LPSPACE1:24;
then ex E being Element of S st
( M . (E ` ) = 0 & E = dom (z (#) a) & z (#) a is_measurable_on E ) by Lem00;
then (lmultCoset M) . z,A = a.e-eq-class_Lp (z (#) a),M,1 by A5, Lem03;
hence (lmultCoset M) . z,A = (lmultCoset M,1) . z,A by A3, A4, VSPDef5X; :: thesis: verum

end;

hence lmultCoset M = lmultCoset M,1 by A1, BINOP_1:2; :: thesis: verum