let X be RealLinearSpace; :: thesis: for A being circled Subset of X
for r being Real st |.r.| = 1 holds
r * A = A
let A be circled Subset of X; :: thesis: for r being Real st |.r.| = 1 holds
r * A = A
let r be Real; :: thesis: ( |.r.| = 1 implies r * A = A )
assume A1: |.r.| = 1 ; :: thesis: r * A = A
hence A2: r * A c= A by Def6; :: according to XBOOLE_0:def 10 :: thesis: A c= r * A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in r * A )
assume A3: x in A ; :: thesis: x in r * A
then reconsider x = x as Point of X ;
A4: r * x in r * A by A3;

per cases ( 0 <= r or r < 0 ) ;

suppose 0 <= r ; :: thesis: x in r * A

then r = 1 by A1, ABSVALUE:def 1;
hence x in r * A by A3, CONVEX1:32; :: thesis: verum

end;

suppose r < 0 ; :: thesis: x in r * A

then |.r.| = - r by ABSVALUE:def 1;
then (- 1) * ((- 1) * x) in r * A by A1, A2, A4;
then ((- 1) * (- 1)) * x in r * A by RLVECT_1:def 7;
hence x in r * A by RLVECT_1:def 8; :: thesis: verum

end;

end;