let V be RealLinearSpace; :: thesis: 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
let M be Subset of V; :: thesis: for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) = (r1 + r2) * M
let r1, r2 be Real; :: thesis: ( r1 >= 0 & r2 >= 0 & M is convex implies (r1 * M) + (r2 * M) = (r1 + r2) * M )
assume ( r1 >= 0 & r2 >= 0 & M is convex ) ; :: thesis: (r1 * M) + (r2 * M) = (r1 + r2) * M
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm10; :: according to XBOOLE_0:def 10 :: thesis: (r1 + r2) * M c= (r1 * M) + (r2 * M)
thus (r1 + r2) * M c= (r1 * M) + (r2 * M) by Th12; :: thesis: verum