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 Th71;

now :: thesis: for z being Element of REAL
for A being Element of CosetSet M holds (lmultCoset M) . (z,A) = (lmultCoset (M,1)) . (z,A)

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 Th71;
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 E -measurable ) by Lm8;
then (lmultCoset M) . (z,A) = a.e-eq-class_Lp ((z (#) a),M,1) by A5, Lm12;
hence (lmultCoset M) . (z,A) = (lmultCoset (M,1)) . (z,A) by A3, A4, Def10; :: thesis: verum

end;

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