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
A3: z1 = r1 and
A4: z2 = r2 and
A5: r1 >= 0 and
A6: 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 = {} & (z1 + z2) * M = {} ) by Th62;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by CONVEX1:40; :: thesis: verum

end;

suppose A7: 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 A8: z1 = 0 ; :: thesis: (z1 * M) + (z2 * M) c= (z1 + z2) * M

then z1 * M = {(0. V)} by A7, Th52;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A8, CONVEX1:35; :: thesis: verum

end;

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

then z2 * M = {(0. V)} by A7, Th52;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A9, CONVEX1:35; :: thesis: verum

end;

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

then r1 + r2 > r1 by A4, A6, XREAL_1:29;
then r1 / (r1 + r2) < 1 by A5, XREAL_1:189;
then ((z1 / (z1 + z2)) * M) + ((1r - (z1 / (z1 + z2))) * M) c= M by A2, A3, A4, A5, A6, A10, Th48;
then A11: (z1 + z2) * (((z1 / (z1 + z2)) * M) + ((1r - (z1 / (z1 + z2))) * M)) c= (z1 + z2) * M by Th61;
1 - (r1 / (r1 + r2)) = ((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2)) by A3, A5, A6, A10, XCMPLX_1:60;
then 1 - (r1 / (r1 + r2)) = ((r1 + r2) - r1) / (r1 + r2) ;
then A12: (z1 + z2) * ((1r - (z1 / (z1 + z2))) * M) = ((z2 / (z1 + z2)) * (z1 + z2)) * M by A3, A4, Th53
.= z2 * M by A3, A4, A5, A6, A10, XCMPLX_1:87 ;
(z1 + z2) * ((z1 / (z1 + z2)) * M) = ((z1 / (z1 + z2)) * (z1 + z2)) * M by Th53
.= z1 * M by A3, A4, A5, A6, A10, XCMPLX_1:87 ;
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by A11, A12, Th54; :: thesis: verum

end;

end;

end;

end;