let V be non empty Abelian add-associative ComplexLinearSpace-like CLSStruct ; :: thesis: for M1, M2, M3 being Subset of V
for z1, z2, z3 being Complex st M1 is convex & M2 is convex & M3 is convex holds
((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex
let M1, M2, M3 be Subset of V; :: thesis: for z1, z2, z3 being Complex st M1 is convex & M2 is convex & M3 is convex holds
((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex
let z1, z2, z3 be Complex; :: thesis: ( M1 is convex & M2 is convex & M3 is convex implies ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex )
assume A1: ( M1 is convex & M2 is convex & M3 is convex ) ; :: thesis: ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex
(z1 * M1) + (z2 * M2) is convex by A1, Th211;
then (1r * ((z1 * M1) + (z2 * M2))) + (z3 * M3) is convex by A1, Th211;
hence ((z1 * M1) + (z2 * M2)) + (z3 * M3) is convex by Lm201; :: thesis: verum