for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)