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) = (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) = (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) = (z1 + z2) * M )
assume ( ex r1, r2 being Real st
( z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0 ) & M is convex ) ; :: thesis: (z1 * M) + (z2 * M) = (z1 + z2) * M
hence (z1 * M) + (z2 * M) c= (z1 + z2) * M by Lm2; :: according to XBOOLE_0:def 10 :: thesis: (z1 + z2) * M c= (z1 * M) + (z2 * M)
thus (z1 + z2) * M c= (z1 * M) + (z2 * M) by Th60; :: thesis: verum