let V be non empty RealLinearSpace-like RLSStruct ; :: thesis: for M being Subset of
for r being Real st M is convex holds
r * M is convex
let M be Subset of ; :: 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
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 ; :: 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 v' being Element of such that
A5: v = r * v' and
A6: v' in M by A4;
consider u' being Element of such that
A7: u = r * u' and
A8: u' in M by A3;
A9: (p * u) + ((1 - p) * v) = ((r * p) * u') + ((1 - p) * (r * v')) by A7, A5, RLVECT_1:def 9
.= ((r * p) * u') + ((r * (1 - p)) * v') by RLVECT_1:def 9
.= (r * (p * u')) + ((r * (1 - p)) * v') by RLVECT_1:def 9
.= (r * (p * u')) + (r * ((1 - p) * v')) by RLVECT_1:def 9
.= r * ((p * u') + ((1 - p) * v')) by RLVECT_1:def 9 ;
(p * u') + ((1 - p) * v') 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