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 () . (z,A) = (lmultCoset (M,1)) . (z,A)
let z be Element of REAL ; :: thesis: for A being Element of CosetSet M holds () . (z,A) = (lmultCoset (M,1)) . (z,A)
let A be Element of CosetSet M; :: thesis: () . (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 ;
then A5: (lmultCoset M) . (z,A) = a.e-eq-class ((z (#) a),M) by LPSPACE1:def 17;
z (#) a in L1_Functions M by ;
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 ;
hence (lmultCoset M) . (z,A) = (lmultCoset (M,1)) . (z,A) by ; :: thesis: verum
end;
hence lmultCoset M = lmultCoset (M,1) by ; :: thesis: verum