:: deftheorem Def5 defines lmultCoset VECTSP10:def 5 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b₄ being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) holds
( b₄ = lmultCoset (V,W) iff for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b₄ . (z,A) = (z * a) + W );