let V be non empty Abelian add-associative ComplexLinearSpace-like CLSStruct ; :: thesis: for M1, M2 being Subset of V
for z1, z2 being Complex st M1 is convex & M2 is convex holds
(z1 * M1) + (z2 * M2) is convex
let M1, M2 be Subset of V; :: thesis: for z1, z2 being Complex st M1 is convex & M2 is convex holds
(z1 * M1) + (z2 * M2) is convex
let z1, z2 be Complex; :: thesis: ( M1 is convex & M2 is convex implies (z1 * M1) + (z2 * M2) is convex )
assume A1: ( M1 is convex & M2 is convex ) ; :: thesis: (z1 * M1) + (z2 * M2) is convex
let u, v be VECTOR of V; :: according to CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in (z1 * M1) + (z2 * M2) & v in (z1 * M1) + (z2 * M2) holds
(z * u) + ((1r - z) * v) in (z1 * M1) + (z2 * M2)
let s be Complex; :: thesis: ( ex r being Real st
( s = r & 0 < r & r < 1 ) & u in (z1 * M1) + (z2 * M2) & v in (z1 * M1) + (z2 * M2) implies (s * u) + ((1r - s) * v) in (z1 * M1) + (z2 * M2) )
assume that
A3: ex p being Real st
( s = p & 0 < p & p < 1 ) and
A4: ( u in (z1 * M1) + (z2 * M2) & v in (z1 * M1) + (z2 * M2) ) ; :: thesis: (s * u) + ((1r - s) * v) in (z1 * M1) + (z2 * M2)
consider u1, u2 being VECTOR of V such that
A6: ( u = u1 + u2 & u1 in z1 * M1 & u2 in z2 * M2 ) by A4;
consider x1 being VECTOR of V such that
A7: ( u1 = z1 * x1 & x1 in M1 ) by A6;
consider x2 being VECTOR of V such that
A8: ( u2 = z2 * x2 & x2 in M2 ) by A6;
consider v1, v2 being VECTOR of V such that
A9: ( v = v1 + v2 & v1 in z1 * M1 & v2 in z2 * M2 ) by A4;
consider y1 being VECTOR of V such that
A10: ( v1 = z1 * y1 & y1 in M1 ) by A9;
consider y2 being VECTOR of V such that
A11: ( v2 = z2 * y2 & y2 in M2 ) by A9;
A12: ( (s * x1) + ((1r - s) * y1) in M1 & (s * x2) + ((1r - s) * y2) in M2 ) by A1, A3, A7, A8, A10, A11, Def202;
(s * u1) + ((1r - s) * v1) = ((z1 * s) * x1) + ((1r - s) * (z1 * y1)) by A7, A10, CLVECT_1:def 2
.= ((z1 * s) * x1) + ((z1 * (1r - s)) * y1) by CLVECT_1:def 2
.= (z1 * (s * x1)) + ((z1 * (1r - s)) * y1) by CLVECT_1:def 2
.= (z1 * (s * x1)) + (z1 * ((1r - s) * y1)) by CLVECT_1:def 2
.= z1 * ((s * x1) + ((1r - s) * y1)) by CLVECT_1:def 2 ;
then A13: (s * u1) + ((1r - s) * v1) in z1 * M1 by A12;
(s * u2) + ((1r - s) * v2) = ((z2 * s) * x2) + ((1r - s) * (z2 * y2)) by A8, A11, CLVECT_1:def 2
.= ((z2 * s) * x2) + ((z2 * (1r - s)) * y2) by CLVECT_1:def 2
.= (z2 * (s * x2)) + ((z2 * (1r - s)) * y2) by CLVECT_1:def 2
.= (z2 * (s * x2)) + (z2 * ((1r - s) * y2)) by CLVECT_1:def 2
.= z2 * ((s * x2) + ((1r - s) * y2)) by CLVECT_1:def 2 ;
then A14: (s * u2) + ((1r - s) * v2) in z2 * M2 by A12;
(s * (u1 + u2)) + ((1r - s) * (v1 + v2)) = ((s * u1) + (s * u2)) + ((1r - s) * (v1 + v2)) by CLVECT_1:def 2
.= ((s * u1) + (s * u2)) + (((1r - s) * v1) + ((1r - s) * v2)) by CLVECT_1:def 2
.= (((s * u1) + (s * u2)) + ((1r - s) * v1)) + ((1r - s) * v2) by RLVECT_1:def 6
.= (((s * u1) + ((1r - s) * v1)) + (s * u2)) + ((1r - s) * v2) by RLVECT_1:def 6
.= ((s * u1) + ((1r - s) * v1)) + ((s * u2) + ((1r - s) * v2)) by RLVECT_1:def 6 ;
hence (s * u) + ((1r - s) * v) in (z1 * M1) + (z2 * M2) by A6, A9, A13, A14; :: thesis: verum