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

proof

let u, v be VECTOR of V; :: thesis: for p being Real st 0 < p & p < 1 & u in r * M & v in r * M holds
(p * u) + ((1 - p) * v) in r * M
let p be Real; :: thesis: ( 0 < p & p < 1 & u in r * M & v in r * M implies (p * u) + ((1 - p) * v) in r * M )
assume that
A2: ( 0 < p & p < 1 ) and
A3: u in r * M and
A4: v in r * M ; :: thesis: (p * u) + ((1 - p) * v) in r * M
consider v9 being Element of V such that
A5: v = r * v9 and
A6: v9 in M by A4;
consider u9 being Element of V such that
A7: u = r * u9 and
A8: u9 in M by A3;
A9: (p * u) + ((1 - p) * v) = ((r * p) * u9) + ((1 - p) * (r * v9)) by A7, A5, RLVECT_1:def 10, RLVECT_1:def 11
.= ((r * p) * u9) + ((r * (1 - p)) * v9) by RLVECT_1:def 10, RLVECT_1:def 11
.= (r * (p * u9)) + ((r * (1 - p)) * v9) by RLVECT_1:def 10, RLVECT_1:def 11
.= (r * (p * u9)) + (r * ((1 - p) * v9)) by RLVECT_1:def 10, RLVECT_1:def 11
.= r * ((p * u9) + ((1 - p) * v9)) by RLVECT_1:def 8 ;
(p * u9) + ((1 - p) * v9) in M by A1, A2, A8, A6, Def2;
hence (p * u) + ((1 - p) * v) in r * M by A9; :: thesis: verum

end;

hence r * M is convex by Def2; :: thesis: verum