let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; :: thesis: for M, N being Subset of V st M is convex & N is convex holds
M + N is convex
let M, N be Subset of V; :: thesis: ( M is convex & N is convex implies M + N is convex )
assume A1: ( M is convex & N is convex ) ; :: thesis: M + N is convex
for u, v being VECTOR of V
for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M + N & v in M + N holds
(z * u) + ((1r - z) * v) in M + N

proof

let u, v be VECTOR of V; :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M + N & v in M + N holds
(z * u) + ((1r - z) * v) in M + N
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & u in M + N & v in M + N implies (z * u) + ((1r - z) * v) in M + N )
assume that
A2: ex r being Real st
( z = r & 0 < r & r < 1 ) and
A3: u in M + N and
A4: v in M + N ; :: thesis: (z * u) + ((1r - z) * v) in M + N
consider x2, y2 being Element of V such that
A5: v = x2 + y2 and
A6: ( x2 in M & y2 in N ) by A4;
consider x1, y1 being Element of V such that
A7: u = x1 + y1 and
A8: ( x1 in M & y1 in N ) by A3;
A9: (z * u) + ((1r - z) * v) = ((z * x1) + (z * y1)) + ((1r - z) * (x2 + y2)) by A7, A5, CLVECT_1:def 2
.= ((z * x1) + (z * y1)) + (((1r - z) * x2) + ((1r - z) * y2)) by CLVECT_1:def 2
.= (((z * x1) + (z * y1)) + ((1r - z) * x2)) + ((1r - z) * y2) by RLVECT_1:def 3
.= (((z * x1) + ((1r - z) * x2)) + (z * y1)) + ((1r - z) * y2) by RLVECT_1:def 3
.= ((z * x1) + ((1r - z) * x2)) + ((z * y1) + ((1r - z) * y2)) by RLVECT_1:def 3 ;
( (z * x1) + ((1r - z) * x2) in M & (z * y1) + ((1r - z) * y2) in N ) by A1, A2, A8, A6;
hence (z * u) + ((1r - z) * v) in M + N by A9; :: thesis: verum

end;

hence M + N is convex ; :: thesis: verum