for V being RealLinearSpace
for M being Subset of V
for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) = (r1 + r2) * M by Lm10, Th12;