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 and

A2: r2 >= 0 and

A3: M is convex ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

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 and

A2: r2 >= 0 and

A3: M is convex ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M

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

end;

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

then
( r1 * M = {} & (r1 + r2) * M = {} )
by Lm7;

hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm8; :: thesis: verum

end;hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm8; :: thesis: verum

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

end;

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

end;

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

then
r1 * M = {(0. V)}
by A4, Lm2;

hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A5, Lm9; :: thesis: verum

end;hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A5, Lm9; :: thesis: verum

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

then
r2 * M = {(0. V)}
by A4, Lm2;

hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A6, Lm9; :: thesis: verum

end;hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A6, Lm9; :: thesis: verum

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

then
r1 + r2 > r1
by A2, XREAL_1:29;

then A8: r1 / (r1 + r2) < 1 by A1, XREAL_1:189;

0 < r1 / (r1 + r2) by A1, A2, A7, XREAL_1:139;

then ((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M) c= M by A3, A8, Th4;

then A9: (r1 + r2) * (((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M)) c= (r1 + r2) * M by Lm6;

1 - (r1 / (r1 + r2)) = ((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2)) by A1, A2, A7, XCMPLX_1:60

.= ((r1 + r2) - r1) / (r1 + r2) by XCMPLX_1:120

.= r2 / (r1 + r2) ;

then A10: (r1 + r2) * ((1 - (r1 / (r1 + r2))) * M) = ((r2 / (r1 + r2)) * (r1 + r2)) * M by Lm4

.= r2 * M by A1, A2, A7, XCMPLX_1:87 ;

(r1 + r2) * ((r1 / (r1 + r2)) * M) = ((r1 / (r1 + r2)) * (r1 + r2)) * M by Lm4

.= r1 * M by A1, A2, A7, XCMPLX_1:87 ;

hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A9, A10, Lm5; :: thesis: verum

end;then A8: r1 / (r1 + r2) < 1 by A1, XREAL_1:189;

0 < r1 / (r1 + r2) by A1, A2, A7, XREAL_1:139;

then ((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M) c= M by A3, A8, Th4;

then A9: (r1 + r2) * (((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M)) c= (r1 + r2) * M by Lm6;

1 - (r1 / (r1 + r2)) = ((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2)) by A1, A2, A7, XCMPLX_1:60

.= ((r1 + r2) - r1) / (r1 + r2) by XCMPLX_1:120

.= r2 / (r1 + r2) ;

then A10: (r1 + r2) * ((1 - (r1 / (r1 + r2))) * M) = ((r2 / (r1 + r2)) * (r1 + r2)) * M by Lm4

.= r2 * M by A1, A2, A7, XCMPLX_1:87 ;

(r1 + r2) * ((r1 / (r1 + r2)) * M) = ((r1 / (r1 + r2)) * (r1 + r2)) * M by Lm4

.= r1 * M by A1, A2, A7, XCMPLX_1:87 ;

hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A9, A10, Lm5; :: thesis: verum