let V be RealLinearSpace; :: thesis: for M1, M2 being Subset of V
for r1, r2 being Real st M1 is circled & M2 is circled holds
(r1 * M1) + (r2 * M2) is circled
let M1, M2 be Subset of V; :: thesis: for r1, r2 being Real st M1 is circled & M2 is circled holds
(r1 * M1) + (r2 * M2) is circled
let r1, r2 be Real; :: thesis: ( M1 is circled & M2 is circled implies (r1 * M1) + (r2 * M2) is circled )
assume that
A1: M1 is circled and
A2: M2 is circled ; :: thesis: (r1 * M1) + (r2 * M2) is circled
let u be VECTOR of V; :: according to CIRCLED1:def 1 :: thesis: for r being Real st abs r <= 1 & u in (r1 * M1) + (r2 * M2) holds
r * u in (r1 * M1) + (r2 * M2)
let p be Real; :: thesis: ( abs p <= 1 & u in (r1 * M1) + (r2 * M2) implies p * u in (r1 * M1) + (r2 * M2) )
assume that
A3: abs p <= 1 and
A4: u in (r1 * M1) + (r2 * M2) ; :: thesis: p * u in (r1 * M1) + (r2 * M2)
u in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A4, RUSUB_4:def 10;
then consider u1, u2 being VECTOR of V such that
A5: ( u = u1 + u2 & u1 in r1 * M1 & u2 in r2 * M2 ) ;
u1 in { (r1 * x) where x is VECTOR of V : x in M1 } by A5, CONVEX1:def 1;
then consider x1 being VECTOR of V such that
A6: ( u1 = r1 * x1 & x1 in M1 ) ;
u2 in { (r2 * x) where x is VECTOR of V : x in M2 } by A5, CONVEX1:def 1;
then consider x2 being VECTOR of V such that
A7: ( u2 = r2 * x2 & x2 in M2 ) ;
A8: ( p * x1 in M1 & p * x2 in M2 ) by A1, A2, A3, A6, A7, Def1;
p * u1 = (r1 * p) * x1 by A6, RLVECT_1:def 9
.= r1 * (p * x1) by RLVECT_1:def 9 ;
then A9: p * u1 in r1 * M1 by A8, RLTOPSP1:1;
p * u2 = (r2 * p) * x2 by A7, RLVECT_1:def 9
.= r2 * (p * x2) by RLVECT_1:def 9 ;
then A10: p * u2 in r2 * M2 by A8, RLTOPSP1:1;
p * (u1 + u2) = (p * u1) + (p * u2) by RLVECT_1:def 9;
then p * (u1 + u2) in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A9, A10;
hence p * u in (r1 * M1) + (r2 * M2) by A5, RUSUB_4:def 10; :: thesis: verum