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) c= (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) c= (r1 + r2) * M
let r1, r2 be Real; :: thesis: ( r1 >= 0 & r2 >= 0 & M is convex implies (r1 * M) + (r2 * M) c= (r1 + r2) * M )
assume that
A1: ( r1 >= 0 & r2 >= 0 ) and
A2: M is convex ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

per cases ( M is empty or not M is empty ) ;

suppose M is empty ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

then ( r1 * M = {} & r2 * M = {} & (r1 + r2) * M = {} ) by Lm7;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm8; :: thesis: verum

end;

suppose A3: not M is empty ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

per cases ( r1 = 0 or r2 = 0 or ( r1 <> 0 & r2 <> 0 ) ) ;

suppose A4: r1 = 0 ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

then r1 * M = {(0. V)} by A3, Lm2;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A4, Lm9; :: thesis: verum

end;

suppose A5: r2 = 0 ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

then r2 * M = {(0. V)} by A3, Lm2;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A5, Lm9; :: thesis: verum

end;

suppose A6: ( r1 <> 0 & r2 <> 0 ) ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

then A7: ( r1 + r2 > 0 + 0 & r1 + r2 > r1 & r1 + r2 > r2 ) by A1, XREAL_1:31;
then A8: ( 0 < r1 / (r1 + r2) & r1 / (r1 + r2) < 1 & 0 < r2 / (r1 + r2) & r2 / (r1 + r2) < 1 ) by A1, A6, XREAL_1:141, XREAL_1:191;
A9: 1 - (r1 / (r1 + r2)) = ((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2)) by A7, XCMPLX_1:60
.= ((r1 + r2) - r1) / (r1 + r2) by XCMPLX_1:121
.= r2 / (r1 + r2) ;
((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M) c= M by A2, A8, Th4;
then A10: (r1 + r2) * (((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M)) c= (r1 + r2) * M by Lm6;
A11: (r1 + r2) * ((r1 / (r1 + r2)) * M) = ((r1 / (r1 + r2)) * (r1 + r2)) * M by Lm4
.= r1 * M by A7, XCMPLX_1:88 ;
(r1 + r2) * ((1 - (r1 / (r1 + r2))) * M) = ((r2 / (r1 + r2)) * (r1 + r2)) * M by A9, Lm4
.= r2 * M by A7, XCMPLX_1:88 ;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A10, A11, Lm5; :: thesis: verum

end;

end;

end;

end;