let V be RealLinearSpace; 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; for r1, r2 being Real st M1 is circled & M2 is circled holds
(r1 * M1) + (r2 * M2) is circled
let r1, r2 be Real; ( M1 is circled & M2 is circled implies (r1 * M1) + (r2 * M2) is circled )
assume that
A1:
M1 is circled
and
A2:
M2 is circled
; (r1 * M1) + (r2 * M2) is circled
let u be VECTOR of V; CIRCLED1:def 1 for r being Real st |.r.| <= 1 & u in (r1 * M1) + (r2 * M2) holds
r * u in (r1 * M1) + (r2 * M2)
let p be Real; ( |.p.| <= 1 & u in (r1 * M1) + (r2 * M2) implies p * u in (r1 * M1) + (r2 * M2) )
assume that
A3:
|.p.| <= 1
and
A4:
u in (r1 * M1) + (r2 * M2)
; 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 9;
then consider u1, u2 being VECTOR of V such that
A5:
u = u1 + u2
and
A6:
u1 in r1 * M1
and
A7:
u2 in r2 * M2
;
u1 in { (r1 * x) where x is VECTOR of V : x in M1 }
by A6, CONVEX1:def 1;
then consider x1 being VECTOR of V such that
A8:
u1 = r1 * x1
and
A9:
x1 in M1
;
A10: p * u1 =
(r1 * p) * x1
by A8, RLVECT_1:def 7
.=
r1 * (p * x1)
by RLVECT_1:def 7
;
u2 in { (r2 * x) where x is VECTOR of V : x in M2 }
by A7, CONVEX1:def 1;
then consider x2 being VECTOR of V such that
A11:
u2 = r2 * x2
and
A12:
x2 in M2
;
A13: p * u2 =
(r2 * p) * x2
by A11, RLVECT_1:def 7
.=
r2 * (p * x2)
by RLVECT_1:def 7
;
reconsider r1 = r1, r2 = r2 as Real ;
p * x2 in M2
by A2, A3, A12;
then A14:
p * u2 in r2 * M2
by A13, RLTOPSP1:1;
p * x1 in M1
by A1, A3, A9;
then A15:
p * u1 in r1 * M1
by A10, RLTOPSP1:1;
p * (u1 + u2) = (p * u1) + (p * u2)
by RLVECT_1:def 5;
then
p * (u1 + u2) in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) }
by A15, A14;
hence
p * u in (r1 * M1) + (r2 * M2)
by A5, RUSUB_4:def 9; verum