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;