let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M, N being Subset of V st M is convex & N is convex holds
for r being Real holds (r * M) + ((1 - r) * N) is convex

let M, N be Subset of V; :: thesis: ( M is convex & N is convex implies for r being Real holds (r * M) + ((1 - r) * N) is convex )
assume that
A1: M is convex and
A2: N is convex ; :: thesis: for r being Real holds (r * M) + ((1 - r) * N) is convex
let r be Real; :: thesis: (r * M) + ((1 - r) * N) is convex
let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) holds
(r * u) + ((1 - r) * v) in (r * M) + ((1 - r) * N)

let p be Real; :: thesis: ( 0 < p & p < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) implies (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) )
assume that
A3: ( 0 < p & p < 1 ) and
A4: u in (r * M) + ((1 - r) * N) and
A5: v in (r * M) + ((1 - r) * N) ; :: thesis: (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N)
A6: u in { (x1 + y1) where x1, y1 is VECTOR of V : ( x1 in r * M & y1 in (1 - r) * N ) } by ;
v in { (x2 + y2) where x2, y2 is VECTOR of V : ( x2 in r * M & y2 in (1 - r) * N ) } by ;
then consider x2, y2 being VECTOR of V such that
A7: v = x2 + y2 and
A8: x2 in r * M and
A9: y2 in (1 - r) * N ;
consider x1, y1 being VECTOR of V such that
A10: u = x1 + y1 and
A11: x1 in r * M and
A12: y1 in (1 - r) * N by A6;
consider mx2 being VECTOR of V such that
A13: x2 = r * mx2 and
A14: mx2 in M by A8;
consider mx1 being VECTOR of V such that
A15: x1 = r * mx1 and
A16: mx1 in M by A11;
A17: (p * x1) + ((1 - p) * x2) = ((p * r) * mx1) + ((1 - p) * (r * mx2)) by
.= ((p * r) * mx1) + (((1 - p) * r) * mx2) by RLVECT_1:def 7
.= (r * (p * mx1)) + (((1 - p) * r) * mx2) by RLVECT_1:def 7
.= (r * (p * mx1)) + (r * ((1 - p) * mx2)) by RLVECT_1:def 7
.= r * ((p * mx1) + ((1 - p) * mx2)) by RLVECT_1:def 5 ;
consider ny2 being VECTOR of V such that
A18: y2 = (1 - r) * ny2 and
A19: ny2 in N by A9;
consider ny1 being VECTOR of V such that
A20: y1 = (1 - r) * ny1 and
A21: ny1 in N by A12;
A22: (p * y1) + ((1 - p) * y2) = ((p * (1 - r)) * ny1) + ((1 - p) * ((1 - r) * ny2)) by
.= ((p * (1 - r)) * ny1) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 7
.= ((1 - r) * (p * ny1)) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 7
.= ((1 - r) * (p * ny1)) + ((1 - r) * ((1 - p) * ny2)) by RLVECT_1:def 7
.= (1 - r) * ((p * ny1) + ((1 - p) * ny2)) by RLVECT_1:def 5 ;
(p * ny1) + ((1 - p) * ny2) in N by A2, A3, A21, A19;
then A23: (p * y1) + ((1 - p) * y2) in (1 - r) * N by A22;
(p * mx1) + ((1 - p) * mx2) in M by A1, A3, A16, A14;
then A24: (p * x1) + ((1 - p) * x2) in { (r * w) where w is VECTOR of V : w in M } by A17;
(p * u) + ((1 - p) * v) = ((p * x1) + (p * y1)) + ((1 - p) * (x2 + y2)) by
.= ((p * x1) + (p * y1)) + (((1 - p) * x2) + ((1 - p) * y2)) by RLVECT_1:def 5
.= (((p * x1) + (p * y1)) + ((1 - p) * x2)) + ((1 - p) * y2) by RLVECT_1:def 3
.= (((p * x1) + ((1 - p) * x2)) + (p * y1)) + ((1 - p) * y2) by RLVECT_1:def 3
.= ((p * x1) + ((1 - p) * x2)) + ((p * y1) + ((1 - p) * y2)) by RLVECT_1:def 3 ;
then (p * u) + ((1 - p) * v) in { (w1 + w2) where w1, w2 is VECTOR of V : ( w1 in r * M & w2 in (1 - r) * N ) } by ;
hence (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) by RUSUB_4:def 9; :: thesis: verum