for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) by Lm5;