theorem :: RLVECT_2:71

for R being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for a being Element of R
for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over R
for v, u, w being Element of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)