theorem :: CONVEX1:37

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) = (r1 * r2) * M by Lm4;