let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M1, M2, M3 being Subset of V

for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds

((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex

let M1, M2, M3 be Subset of V; :: thesis: for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds

((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex

let r1, r2, r3 be Real; :: thesis: ( M1 is convex & M2 is convex & M3 is convex implies ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex )

assume that

A1: ( M1 is convex & M2 is convex ) and

A2: M3 is convex ; :: thesis: ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex

(r1 * M1) + (r2 * M2) is convex by A1, Th11;

then (1 * ((r1 * M1) + (r2 * M2))) + (r3 * M3) is convex by A2, Th11;

hence ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex by Lm1; :: thesis: verum

for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds

((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex

let M1, M2, M3 be Subset of V; :: thesis: for r1, r2, r3 being Real st M1 is convex & M2 is convex & M3 is convex holds

((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex

let r1, r2, r3 be Real; :: thesis: ( M1 is convex & M2 is convex & M3 is convex implies ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex )

assume that

A1: ( M1 is convex & M2 is convex ) and

A2: M3 is convex ; :: thesis: ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex

(r1 * M1) + (r2 * M2) is convex by A1, Th11;

then (1 * ((r1 * M1) + (r2 * M2))) + (r3 * M3) is convex by A2, Th11;

hence ((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex by Lm1; :: thesis: verum