let X be RealLinearSpace; :: thesis: for A, B being circled Subset of X holds A + B is circled
let A, B be circled Subset of X; :: thesis: A + B is circled
A1: A + B = { (u + v) where u, v is Point of X : ( u in A & v in B ) } by RUSUB_4:def 9;
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( |.r.| <= 1 implies r * (A + B) c= A + B )
assume |.r.| <= 1 ; :: thesis: r * (A + B) c= A + B
then A2: ( r * A c= A & r * B c= B ) by Def6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (A + B) or x in A + B )
assume x in r * (A + B) ; :: thesis: x in A + B
then consider x9 being Point of X such that
A3: x = r * x9 and
A4: x9 in A + B ;
consider u, v being Point of X such that
A5: x9 = u + v and
A6: ( u in A & v in B ) by A1, A4;
A7: ( r * u in r * A & r * v in r * B ) by A6;
x = (r * u) + (r * v) by A3, A5, RLVECT_1:def 5;
hence x in A + B by A2, A7, Th3; :: thesis: verum