theorem :: RLVECT_2:70

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 being Element of V holds a * (Sum <*v,u*>) = (a * v) + (a * u)