:: deftheorem Def19 defines Pre-L-CSpace LPSPACC1:def 19 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct holds
( b₄ = Pre-L-CSpace M iff ( the carrier of b₄ = CCosetSet M & the addF of b₄ = addCCoset M & 0. b₄ = zeroCCoset M & the Mult of b₄ = lmultCCoset M ) );