:: deftheorem Def17 defines lmultCoset LPSPACE1:def 17 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Function of [:REAL,(CosetSet M):],(CosetSet M) holds
( b₄ = lmultCoset M iff for z being Real
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b₄ . (z,A) = a.e-eq-class ((z (#) f),M) );