let V be RealLinearSpace; :: thesis: for M being Subset of V
for r being Real st M is circled holds
r * M is circled
let M be Subset of V; :: thesis: for r being Real st M is circled holds
r * M is circled
let r be Real; :: thesis: ( M is circled implies r * M is circled )
assume A1: M is circled ; :: thesis: r * M is circled
for u being VECTOR of V
for p being Real st |.p.| <= 1 & u in r * M holds
p * u in r * M

proof

let u be VECTOR of V; :: thesis: for p being Real st |.p.| <= 1 & u in r * M holds
p * u in r * M
let p be Real; :: thesis: ( |.p.| <= 1 & u in r * M implies p * u in r * M )
assume that
A2: |.p.| <= 1 and
A3: u in r * M ; :: thesis: p * u in r * M
u in { (r * w) where w is Element of V : w in M } by A3, CONVEX1:def 1;
then consider u9 being Element of V such that
A4: u = r * u9 and
A5: u9 in M ;
A6: p * u = (r * p) * u9 by A4, RLVECT_1:def 7
.= r * (p * u9) by RLVECT_1:def 7 ;
p * u9 in M by A1, A2, A5;
hence p * u in r * M by A6, RLTOPSP1:1; :: thesis: verum

end;

hence r * M is circled ; :: thesis: verum