theorem :: VECTSP_1:23

for F being non empty right_complementable Abelian add-associative right_zeroed associative right_unital well-unital distributive doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F
for x being Element of F
for v, w being Element of V holds x * (v - w) = (x * v) - (x * w)