:: deftheorem Def18 defines lmultCCoset LPSPACC1:def 18 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M) holds
( b₄ = lmultCCoset M iff for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b₄ . (z,A) = a.e-Ceq-class ((z (#) f),M) );