let V be ComplexLinearSpace; :: thesis: for M being Subset of V
for z1, z2 being Complex st ex r1, r2 being Real st
( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex holds
(z1 * M) + (z2 * M) c= (z1 + z2) * M
let M be Subset of V; :: thesis: for z1, z2 being Complex st ex r1, r2 being Real st
( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex holds
(z1 * M) + (z2 * M) c= (z1 + z2) * M
let z1, z2 be Complex; :: thesis: ( ex r1, r2 being Real st
( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex implies (z1 * M) + (z2 * M) c= (z1 + z2) * M )
assume that
A1: ex r1, r2 being Real st
( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) and
A2: M is convex ; :: thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M
consider r1, r2 being Real such that
B1: ( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) by A1;

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

suppose M is empty ; :: thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M

then ( z1 * M = {} & z2 * M = {} & (z1 + z2) * M = {} ) by Lm207;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by Lm208; :: thesis: verum

end;

suppose A3: not M is empty ; :: thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M

per cases ( z1 = 0 or z2 = 0 or ( z1 <> 0 & z2 <> 0 ) ) ;

suppose A4: z1 = 0 ; :: thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M

then z1 * M = {(0. V)} by A3, Lm202;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A4, Lm209; :: thesis: verum

end;

suppose A5: z2 = 0 ; :: thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M

then z2 * M = {(0. V)} by A3, Lm202;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A5, Lm209; :: thesis: verum

end;

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

then A7: ( r1 + r2 > 0 + 0 & r1 + r2 > r1 & r1 + r2 > r2 ) by B1, XREAL_1:31;
then ( 0 < r1 / (r1 + r2) & r1 / (r1 + r2) < 1 & 0 < r2 / (r1 + r2) & r2 / (r1 + r2) < 1 ) by B1, A6, XREAL_1:191;
then ((z1 / (z1 + z2)) * M) + ((1r - (z1 / (z1 + z2))) * M) c= M by B1, A2, Th204;
then A10: (z1 + z2) * (((z1 / (z1 + z2)) * M) + ((1r - (z1 / (z1 + z2))) * M)) c= (z1 + z2) * M by Lm206;
A11: (z1 + z2) * ((z1 / (z1 + z2)) * M) = ((z1 / (z1 + z2)) * (z1 + z2)) * M by Lm204
.= z1 * M by B1, A7, XCMPLX_1:88 ;
1 - (r1 / (r1 + r2)) = ((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2)) by A7, XCMPLX_1:60;
then 1 - (r1 / (r1 + r2)) = ((r1 + r2) - r1) / (r1 + r2) ;
then (z1 + z2) * ((1r - (z1 / (z1 + z2))) * M) = ((z2 / (z1 + z2)) * (z1 + z2)) * M by B1, Lm204
.= z2 * M by B1, A7, XCMPLX_1:88 ;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A10, A11, Lm205; :: thesis: verum

end;

end;

end;

end;