:: CIRCLED1 semantic presentation

begin

Lm1:  for V being non empty RLSStruct
for M, N being Subset of V
for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
proof
let V be non empty RLSStruct ; ::_thesis: for M, N being Subset of V
for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
let M, N be Subset of V; ::_thesis: for x, y being VECTOR of V st x in M & y in N holds
x - y in M - N
let x, y be VECTOR of V; ::_thesis: ( x in M & y in N implies x - y in M - N )
 M - N =  {  (u - v) where u, v is VECTOR of V : ( u in M & v in N )  }  by RUSUB_5:def_2;
hence  ( x in M & y in N implies x - y in M - N ) ; ::_thesis: verum
end;

theorem Th1: :: CIRCLED1:1
for V being RealLinearSpace
for A, B being circled Subset of V holds A - B is circled
proof
let V be RealLinearSpace; ::_thesis: for A, B being circled Subset of V holds A - B is circled
let A, B be circled Subset of V; ::_thesis: A - B is circled
A1: A - B =  {  (u - v) where u, v is VECTOR of V : ( u in A & v in B )  }  by RUSUB_5:def_2;
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( not abs r <= 1 or r * (A - B) c= A - B )
assume  abs r <= 1 ; ::_thesis: r * (A - B) c= A - B
then A2: ( r * A c= A & r * B c= B ) by RLTOPSP1:def_6;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (A - B) or x in A - B )
assume A3: x in r * (A - B) ; ::_thesis: x in A - B
 r * (A - B) =  {  (r * v) where v is VECTOR of V : v in A - B  }  by CONVEX1:def_1;
then consider x9 being VECTOR of V such that
A4: x = r * x9 and
A5: x9 in A - B by A3;
consider u, v being VECTOR of V such that
A6: x9 = u - v and
A7: ( u in A & v in B ) by A1, A5;
A8: ( r * u in r * A & r * v in r * B ) by A7, RLTOPSP1:1;
 x = (r * u) - (r * v) by A4, A6, RLVECT_1:34;
hence  x in A - B by A2, A8, Lm1; ::_thesis: verum
end;

registration
let V be RealLinearSpace;
let M, N be circled Subset of V;
clusterM - N ->  circled ;
coherence
 M - N is circled by Th1;
end;

definition
let V be non empty RLSStruct ;
let M be Subset of V;
redefine attr M is circled  means :Def1: :: CIRCLED1:def 1
 for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M;
compatibility
 ( M is circled iff for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M )
proof
thus  ( M is circled implies for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M ) ::_thesis: ( ( for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M ) implies M is circled )
proof
assume A1: M is circled ; ::_thesis: for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M
let u be VECTOR of V; ::_thesis: for r being Real st abs r <= 1 & u in M holds
r * u in M
let r be Real; ::_thesis: ( abs r <= 1 & u in M implies r * u in M )
assume  abs r <= 1 ; ::_thesis: ( not u in M or r * u in M )
then A2: r * M c= M by A1, RLTOPSP1:def_6;
assume  u in M ; ::_thesis: r * u in M
then  r * u in r * M by RLTOPSP1:1;
hence  r * u in M by A2; ::_thesis: verum
end;
assume A3: for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M ; ::_thesis: M is circled
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( not abs r <= 1 or r * M c= M )
assume A4: abs r <= 1 ; ::_thesis: r * M c= M
 for x being Element of V st x in r * M holds
x in M
proof
let x be Element of V; ::_thesis: ( x in r * M implies x in M )
assume  x in r * M ; ::_thesis: x in M
then consider u being Element of V such that
A5: x = u and
A6: u in r * M ;
 u in  {  (r * w) where w is Element of V : w in M  }  by A6, CONVEX1:def_1;
then  ex w1 being Element of V st
( u = r * w1 & w1 in M ) ;
hence  x in M by A3, A4, A5; ::_thesis: verum
end;
hence  r * M c= M by SUBSET_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines circled CIRCLED1:def_1_:_
 for V being non empty RLSStruct
for M being Subset of V holds
( M is circled iff for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M );

theorem Th2: :: CIRCLED1:2
for V being RealLinearSpace
for M being Subset of V
for r being Real st M is circled holds
r * M is circled
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V
for r being Real st M is circled holds
r * M is circled
let M be Subset of V; ::_thesis: for r being Real st M is circled holds
r * M is circled
let r be Real; ::_thesis: ( M is circled implies r * M is circled )
assume A1: M is circled ; ::_thesis: r * M is circled
 for u being VECTOR of V
for p being Real st abs p <= 1 & u in r * M holds
p * u in r * M
proof
let u be VECTOR of V; ::_thesis: for p being Real st abs p <= 1 & u in r * M holds
p * u in r * M
let p be Real; ::_thesis: ( abs p <= 1 & u in r * M implies p * u in r * M )
assume that
A2: abs p <= 1 and
A3: u in r * M ; ::_thesis: p * u in r * M
 u in  {  (r * w) where w is Element of V : w in M  }  by A3, CONVEX1:def_1;
then consider u9 being Element of V such that
A4: u = r * u9 and
A5: u9 in M ;
A6: p * u = (r * p) * u9 by A4, RLVECT_1:def_7
.= r * (p * u9) by RLVECT_1:def_7 ;
 p * u9 in M by A1, A2, A5, Def1;
hence  p * u in r * M by A6, RLTOPSP1:1; ::_thesis: verum
end;
hence  r * M is circled by Def1; ::_thesis: verum
end;

theorem Th3: :: CIRCLED1:3
for V being 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
proof
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_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 ;
 p * x2 in M2 by A2, A3, A12, Def1;
then A14: p * u2 in r2 * M2 by A13, RLTOPSP1:1;
 p * x1 in M1 by A1, A3, A9, Def1;
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; ::_thesis: verum
end;

theorem :: CIRCLED1:4
for V being RealLinearSpace
for M1, M2, M3 being Subset of V
for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
proof
let V be RealLinearSpace; ::_thesis: for M1, M2, M3 being Subset of V
for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
let M1, M2, M3 be Subset of V; ::_thesis: for r1, r2, r3 being Real st M1 is circled & M2 is circled & M3 is circled holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
let r1, r2, r3 be Real; ::_thesis: ( M1 is circled & M2 is circled & M3 is circled implies ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled )
assume that
A1: ( M1 is circled & M2 is circled ) and
A2: M3 is circled ; ::_thesis: ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled
 (r1 * M1) + (r2 * M2) is circled by A1, Th3;
then  (1 * ((r1 * M1) + (r2 * M2))) + (r3 * M3) is circled by A2, Th3;
hence  ((r1 * M1) + (r2 * M2)) + (r3 * M3) is circled by CONVEX1:32; ::_thesis: verum
end;

theorem :: CIRCLED1:5
for V being RealLinearSpace holds Up ((0). V) is circled
proof
let V be RealLinearSpace; ::_thesis: Up ((0). V) is circled
let u be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & u in Up ((0). V) holds
r * u in Up ((0). V)
let r be Real; ::_thesis: ( abs r <= 1 & u in Up ((0). V) implies r * u in Up ((0). V) )
assume that
 abs r <= 1 and
A1: u in Up ((0). V) ; ::_thesis: r * u in Up ((0). V)
 u in the carrier of ((0). V) by A1, RUSUB_4:def_5;
then  u in {(0. V)} by RLSUB_1:def_3;
then  u = 0. V by TARSKI:def_1;
then  r * u = 0. V by RLVECT_1:10;
then  r * u in {(0. V)} by TARSKI:def_1;
then  r * u in the carrier of ((0). V) by RLSUB_1:def_3;
hence  r * u in Up ((0). V) by RUSUB_4:def_5; ::_thesis: verum
end;

theorem Th6: :: CIRCLED1:6
for V being RealLinearSpace holds Up ((Omega). V) is circled
proof
let V be RealLinearSpace; ::_thesis: Up ((Omega). V) is circled
let u be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & u in Up ((Omega). V) holds
r * u in Up ((Omega). V)
let r be Real; ::_thesis: ( abs r <= 1 & u in Up ((Omega). V) implies r * u in Up ((Omega). V) )
 (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) by RLSUB_1:def_4;
then  r * u in the carrier of ((Omega). V) ;
hence  ( abs r <= 1 & u in Up ((Omega). V) implies r * u in Up ((Omega). V) ) by RUSUB_4:def_5; ::_thesis: verum
end;

theorem :: CIRCLED1:7
for V being RealLinearSpace
for M, N being circled Subset of V holds M /\ N is circled
proof
let V be RealLinearSpace; ::_thesis: for M, N being circled Subset of V holds M /\ N is circled
let M, N be circled Subset of V; ::_thesis: M /\ N is circled
let x be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & x in M /\ N holds
r * x in M /\ N
let r be Real; ::_thesis: ( abs r <= 1 & x in M /\ N implies r * x in M /\ N )
assume that
A1: abs r <= 1 and
A2: x in M /\ N ; ::_thesis: r * x in M /\ N
 x in N by A2, XBOOLE_0:def_4;
then A3: r * x in N by A1, Def1;
 x in M by A2, XBOOLE_0:def_4;
then  r * x in M by A1, Def1;
hence  r * x in M /\ N by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: CIRCLED1:8
for V being RealLinearSpace
for M, N being circled Subset of V holds M \/ N is circled
proof
let V be RealLinearSpace; ::_thesis: for M, N being circled Subset of V holds M \/ N is circled
let M, N be circled Subset of V; ::_thesis: M \/ N is circled
let x be VECTOR of V; :: according to CIRCLED1:def_1 ::_thesis: for r being Real st abs r <= 1 & x in M \/ N holds
r * x in M \/ N
let r be Real; ::_thesis: ( abs r <= 1 & x in M \/ N implies r * x in M \/ N )
assume that
A1: abs r <= 1 and
A2: x in M \/ N ; ::_thesis: r * x in M \/ N
 ( x in M or x in N ) by A2, XBOOLE_0:def_3;
then  ( r * x in M or r * x in N ) by A1, Def1;
hence  r * x in M \/ N by XBOOLE_0:def_3; ::_thesis: verum
end;

begin

definition
let V be non empty RLSStruct ;
let M be Subset of V;
func Circled-Family M ->  Subset-Family of V means :Def2: :: CIRCLED1:def 2
 for N being Subset of V holds
( N in it iff ( N is circled & M c= N ) );
existence
 ex b1 being Subset-Family of V st
for N being Subset of V holds
( N in b1 iff ( N is circled & M c= N ) )
proof
defpred S1[ Subset of V] means ( $1 is circled & M c= $1 );
thus  ex F being Subset-Family of V st
for N being Subset of V holds
( N in F iff S1[N] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of V st ( for N being Subset of V holds
( N in b1 iff ( N is circled & M c= N ) ) ) & ( for N being Subset of V holds
( N in b2 iff ( N is circled & M c= N ) ) ) holds
b1 = b2
proof
let SF, SG be Subset-Family of V; ::_thesis: ( ( for N being Subset of V holds
( N in SF iff ( N is circled & M c= N ) ) ) & ( for N being Subset of V holds
( N in SG iff ( N is circled & M c= N ) ) ) implies SF = SG )
assume that
A1: for N being Subset of V holds
( N in SF iff ( N is circled & M c= N ) ) and
A2: for N being Subset of V holds
( N in SG iff ( N is circled & M c= N ) ) ; ::_thesis: SF = SG
 for Y being Subset of V holds
( Y in SF iff Y in SG )
proof
let Y be Subset of V; ::_thesis: ( Y in SF iff Y in SG )
hereby  ::_thesis: ( Y in SG implies Y in SF )
assume  Y in SF ; ::_thesis: Y in SG
then  ( Y is circled & M c= Y ) by A1;
hence  Y in SG by A2; ::_thesis: verum
end;
assume  Y in SG ; ::_thesis: Y in SF
then  ( Y is circled & M c= Y ) by A2;
hence  Y in SF by A1; ::_thesis: verum
end;
hence  SF = SG by SETFAM_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Circled-Family CIRCLED1:def_2_:_
 for V being non empty RLSStruct
for M being Subset of V
for b3 being Subset-Family of V holds
( b3 = Circled-Family M iff for N being Subset of V holds
( N in b3 iff ( N is circled & M c= N ) ) );

definition
let V be RealLinearSpace;
let M be Subset of V;
func Cir M ->  circled Subset of V equals :: CIRCLED1:def 3
 meet (Circled-Family M);
coherence
 meet (Circled-Family M) is circled Subset of V
proof
 for N being Subset of V st N in Circled-Family M holds
N is circled by Def2;
then  Circled-Family M is circled-membered by RLTOPSP1:def_7;
hence  meet (Circled-Family M) is circled Subset of V by RLTOPSP1:30; ::_thesis: verum
end;
end;

:: deftheorem  defines Cir CIRCLED1:def_3_:_
 for V being RealLinearSpace
for M being Subset of V holds Cir M = meet (Circled-Family M);

registration
let V be RealLinearSpace;
let M be Subset of V;
cluster Circled-Family M ->  non empty ;
coherence
 not Circled-Family M is empty
proof
A1: M c= Up ((Omega). V)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in M or u in Up ((Omega). V) )
assume  u in M ; ::_thesis: u in Up ((Omega). V)
then reconsider u = u as Element of V ;
 u in the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) ;
then  u in the carrier of ((Omega). V) by RLSUB_1:def_4;
hence  u in Up ((Omega). V) by RUSUB_4:def_5; ::_thesis: verum
end;
 Up ((Omega). V) is circled by Th6;
hence  not Circled-Family M is empty by A1, Def2; ::_thesis: verum
end;
end;

theorem Th9: :: CIRCLED1:9
for V being RealLinearSpace
for M1, M2 being Subset of V st M1 c= M2 holds
Circled-Family M2 c= Circled-Family M1
proof
let V be RealLinearSpace; ::_thesis: for M1, M2 being Subset of V st M1 c= M2 holds
Circled-Family M2 c= Circled-Family M1
let M1, M2 be Subset of V; ::_thesis: ( M1 c= M2 implies Circled-Family M2 c= Circled-Family M1 )
assume A1: M1 c= M2 ; ::_thesis: Circled-Family M2 c= Circled-Family M1
let M be set ; :: according to TARSKI:def_3 ::_thesis: ( not M in Circled-Family M2 or M in Circled-Family M1 )
assume A2: M in Circled-Family M2 ; ::_thesis: M in Circled-Family M1
then reconsider M = M as Subset of V ;
 M2 c= M by A2, Def2;
then A3: M1 c= M by A1, XBOOLE_1:1;
 M is circled by A2, Def2;
hence  M in Circled-Family M1 by A3, Def2; ::_thesis: verum
end;

theorem :: CIRCLED1:10
for V being RealLinearSpace
for M1, M2 being Subset of V st M1 c= M2 holds
Cir M1 c= Cir M2
proof
let V be RealLinearSpace; ::_thesis: for M1, M2 being Subset of V st M1 c= M2 holds
Cir M1 c= Cir M2
let M1, M2 be Subset of V; ::_thesis: ( M1 c= M2 implies Cir M1 c= Cir M2 )
assume  M1 c= M2 ; ::_thesis: Cir M1 c= Cir M2
then  Circled-Family M2 c= Circled-Family M1 by Th9;
then A1: meet (Circled-Family M1) c= meet (Circled-Family M2) by SETFAM_1:6;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cir M1 or x in Cir M2 )
assume  x in Cir M1 ; ::_thesis: x in Cir M2
hence  x in Cir M2 by A1; ::_thesis: verum
end;

theorem Th11: :: CIRCLED1:11
for V being RealLinearSpace
for M being Subset of V holds M c= Cir M
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V holds M c= Cir M
let M be Subset of V; ::_thesis: M c= Cir M
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in M or u in Cir M )
assume A1: u in M ; ::_thesis: u in Cir M
 for Y being set st Y in Circled-Family M holds
u in Y
proof
let Y be set ; ::_thesis: ( Y in Circled-Family M implies u in Y )
assume A2: Y in Circled-Family M ; ::_thesis: u in Y
then reconsider Y = Y as Subset of V ;
 M c= Y by A2, Def2;
hence  u in Y by A1; ::_thesis: verum
end;
hence  u in Cir M by SETFAM_1:def_1; ::_thesis: verum
end;

theorem Th12: :: CIRCLED1:12
for V being RealLinearSpace
for M being Subset of V
for N being circled Subset of V st M c= N holds
Cir M c= N
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V
for N being circled Subset of V st M c= N holds
Cir M c= N
let M be Subset of V; ::_thesis: for N being circled Subset of V st M c= N holds
Cir M c= N
let N be circled Subset of V; ::_thesis: ( M c= N implies Cir M c= N )
assume  M c= N ; ::_thesis: Cir M c= N
then  N in Circled-Family M by Def2;
hence  Cir M c= N by SETFAM_1:3; ::_thesis: verum
end;

theorem :: CIRCLED1:13
for V being RealLinearSpace
for M being circled Subset of V holds Cir M = M
proof
let V be RealLinearSpace; ::_thesis: for M being circled Subset of V holds Cir M = M
let M be circled Subset of V; ::_thesis: Cir M = M
thus  Cir M c= M by Th12; :: according to XBOOLE_0:def_10 ::_thesis: M c= Cir M
thus  M c= Cir M by Th11; ::_thesis: verum
end;

theorem Th14: :: CIRCLED1:14
for V being RealLinearSpace holds Cir ({} V) = {}
proof
let V be RealLinearSpace; ::_thesis: Cir ({} V) = {}
 {} V in Circled-Family ({} V) by Def2;
hence  Cir ({} V) = {} by SETFAM_1:4; ::_thesis: verum
end;

theorem :: CIRCLED1:15
for V being RealLinearSpace
for M being Subset of V
for r being Real holds r * (Cir M) = Cir (r * M)
proof
let V be RealLinearSpace; ::_thesis: for M being Subset of V
for r being Real holds r * (Cir M) = Cir (r * M)
let M be Subset of V; ::_thesis: for r being Real holds r * (Cir M) = Cir (r * M)
let r be Real; ::_thesis: r * (Cir M) = Cir (r * M)
thus  r * (Cir M) c= Cir (r * M) :: according to XBOOLE_0:def_10 ::_thesis: Cir (r * M) c= r * (Cir M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) )
percases ( r = 0 or r <> 0 ) ;
supposeA1: r = 0 ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) )
percases ( M = {} or M <> {} ) ;
suppose M = {} ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) )
then  M = {} V ;
then  Cir M = {} by Th14;
hence  ( not x in r * (Cir M) or x in Cir (r * M) ) by CONVEX1:33; ::_thesis: verum
end;
supposeA2: M <> {} ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) )
then  r * M = {(0. V)} by A1, CONVEX1:34;
then A3: {(0. V)} c= Cir (r * M) by Th11;
 Cir M <> {} by A2, Th11, XBOOLE_1:3;
then  r * (Cir M) = {(0. V)} by A1, CONVEX1:34;
hence  ( not x in r * (Cir M) or x in Cir (r * M) ) by A3; ::_thesis: verum
end;
end;
end;
supposeA4: r <> 0 ; ::_thesis: ( not x in r * (Cir M) or x in Cir (r * M) )
A5: r * (Cir M) =  {  (r * v) where v is Point of V : v in Cir M  }  by CONVEX1:def_1;
assume  x in r * (Cir M) ; ::_thesis: x in Cir (r * M)
then consider v being Point of V such that
A6: x = r * v and
A7: v in Cir M by A5;
 for W being set st W in Circled-Family (r * M) holds
r * v in W
proof
let W be set ; ::_thesis: ( W in Circled-Family (r * M) implies r * v in W )
assume A8: W in Circled-Family (r * M) ; ::_thesis: r * v in W
then reconsider W = W as Subset of V ;
 r * M c= W by A8, Def2;
then  (r ") * (r * M) c= (r ") * W by CONVEX1:39;
then  ((r ") * r) * M c= (r ") * W by CONVEX1:37;
then  1 * M c= (r ") * W by A4, XCMPLX_0:def_7;
then A9: M c= (r ") * W by CONVEX1:32;
 W is circled by A8, Def2;
then  (r ") * W is circled by Th2;
then  (r ") * W in Circled-Family M by A9, Def2;
then  ( (r ") * W =  {  ((r ") * w) where w is Point of V : w in W  }  & v in (r ") * W ) by A7, CONVEX1:def_1, SETFAM_1:def_1;
then consider w being Point of V such that
A10: v = (r ") * w and
A11: w in W ;
r * v = (r * (r ")) * w by A10, RLVECT_1:def_7
.= 1 * w by A4, XCMPLX_0:def_7
.= w by RLVECT_1:def_8 ;
hence  r * v in W by A11; ::_thesis: verum
end;
hence  x in Cir (r * M) by A6, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
 ( r * M c= r * (Cir M) & r * (Cir M) is circled ) by Th2, Th11, CONVEX1:39;
hence  Cir (r * M) c= r * (Cir M) by Th12; ::_thesis: verum
end;

begin

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
attrL is circled  means :Def4: :: CIRCLED1:def 4
 ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) );
end;

:: deftheorem Def4 defines circled CIRCLED1:def_4_:_
 for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is circled iff ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) ) );

theorem Th16: :: CIRCLED1:16
for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
Carrier L <> {}
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is circled holds
Carrier L <> {}
let L be Linear_Combination of V; ::_thesis: ( L is circled implies Carrier L <> {} )
assume that
A1: L is circled and
A2: Carrier L = {} ; ::_thesis: contradiction
consider F being FinSequence of the carrier of V such that
A3: ( F is one-to-one & rng F = Carrier L ) and
A4: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4;
consider f being FinSequence of REAL  such that
A5: ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A4;
 len F = 0 by A2, A3, CARD_1:27, FINSEQ_4:62;
then  f = <*> the carrier of V by A5;
hence  contradiction by A5, RVSUM_1:72; ::_thesis: verum
end;

theorem Th17: :: CIRCLED1:17
for V being RealLinearSpace
for L being Linear_Combination of V
for v being VECTOR of V st L is circled & L . v <= 0 holds
not v in Carrier L
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V
for v being VECTOR of V st L is circled & L . v <= 0 holds
not v in Carrier L
let L be Linear_Combination of V; ::_thesis: for v being VECTOR of V st L is circled & L . v <= 0 holds
not v in Carrier L
let v be VECTOR of V; ::_thesis: ( L is circled & L . v <= 0 implies not v in Carrier L )
assume that
A1: L is circled and
A2: L . v <= 0 ; ::_thesis: not v in Carrier L
percases ( L . v = 0 or L . v < 0 ) by A2;
suppose L . v = 0 ; ::_thesis: not v in Carrier L
hence  not v in Carrier L by RLVECT_2:19; ::_thesis: verum
end;
supposeA3: L . v < 0 ; ::_thesis: not v in Carrier L
now__::_thesis:_not_v_in_Carrier_L
consider F being FinSequence of the carrier of V such that
 F is one-to-one and
A4: rng F = Carrier L and
A5: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4;
assume  v in Carrier L ; ::_thesis: contradiction
then consider n being set  such that
A6: n in dom F and
A7: F . n = v by A4, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
consider f being FinSequence of REAL  such that
A8: len f = len F and
 Sum f = 1 and
A9: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A5;
 n in Seg (len F) by A6, FINSEQ_1:def_3;
then A10: n in dom f by A8, FINSEQ_1:def_3;
then  L . v = f . n by A9, A7;
hence  contradiction by A3, A9, A10; ::_thesis: verum
end;
hence  not v in Carrier L ; ::_thesis: verum
end;
end;
end;

theorem :: CIRCLED1:18
for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
L <> ZeroLC V
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is circled holds
L <> ZeroLC V
let L be Linear_Combination of V; ::_thesis: ( L is circled implies L <> ZeroLC V )
assume that
A1: L is circled and
A2: L = ZeroLC V ; ::_thesis: contradiction
 Carrier L <> {} by A1, Th16;
hence  contradiction by A2, RLVECT_2:def_5; ::_thesis: verum
end;

registration
let V be RealLinearSpace;
clusterV10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() circled for Linear_Combination of V;
existence
 ex b1 being Linear_Combination of V st b1 is circled
proof
set u = the Element of V;
consider L being Linear_Combination of { the Element of V} such that
A1: L . the Element of V = 1 by RLVECT_4:37;
take  L ; ::_thesis: L is circled
 L is circled
proof
take  <* the Element of V*> ; :: according to CIRCLED1:def_4 ::_thesis: ( <* the Element of V*> is one-to-one & rng <* the Element of V*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) )
A2: ex f being FinSequence of REAL st
( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) )
proof
reconsider f = <*1*> as FinSequence of REAL ;
take  f ; ::_thesis: ( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) )
A3: for n being Nat st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) )
assume  n in dom f ; ::_thesis: ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 )
then  n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A4: n = 1 by TARSKI:def_1;
then f . n = L . the Element of V by A1, FINSEQ_1:40
.= L . (<* the Element of V*> . n) by A4, FINSEQ_1:40 ;
hence  ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) by A4, FINSEQ_1:40; ::_thesis: verum
end;
len <*1*> = 1 by FINSEQ_1:39
.= len <* the Element of V*> by FINSEQ_1:39 ;
hence  ( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) by A3, FINSOP_1:11; ::_thesis: verum
end;
 the Element of V in  {  w where w is Element of V : L . w <> 0  }  by A1;
then  the Element of V in Carrier L by RLVECT_2:def_4;
then  ( Carrier L c= { the Element of V} & { the Element of V} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31;
then  Carrier L = { the Element of V} by XBOOLE_0:def_10;
hence  ( <* the Element of V*> is one-to-one & rng <* the Element of V*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <* the Element of V*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ) ) ) by A2, FINSEQ_1:38, FINSEQ_3:93; ::_thesis: verum
end;
hence  L is circled ; ::_thesis: verum
end;
end;

definition
let V be RealLinearSpace;
mode circled_Combination of V is circled Linear_Combination of V;
end;

registration
let V be RealLinearSpace;
let M be non empty Subset of V;
clusterV10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() circled for Linear_Combination of M;
existence
 ex b1 being Linear_Combination of M st b1 is circled
proof
consider u being set  such that
A1: u in M by XBOOLE_0:def_1;
reconsider u = u as Element of V by A1;
consider L being Linear_Combination of {u} such that
A2: L . u = 1 by RLVECT_4:37;
 {u} c= M by A1, ZFMISC_1:31;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
take  L ; ::_thesis: L is circled
 L is circled
proof
take  <*u*> ; :: according to CIRCLED1:def_4 ::_thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) )
A3: ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )
proof
reconsider f = <*1*> as FinSequence of REAL ;
take  f ; ::_thesis: ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )
A4: for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (<*u*> . n) & f . n >= 0 ) )
assume  n in dom f ; ::_thesis: ( f . n = L . (<*u*> . n) & f . n >= 0 )
then  n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A5: n = 1 by TARSKI:def_1;
then  f . n = 1 by FINSEQ_1:40;
hence  ( f . n = L . (<*u*> . n) & f . n >= 0 ) by A2, A5, FINSEQ_1:40; ::_thesis: verum
end;
len <*1*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39 ;
hence  ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) by A4, FINSOP_1:11; ::_thesis: verum
end;
 u in  {  w where w is Element of V : L . w <> 0  }  by A2;
then  u in Carrier L by RLVECT_2:def_4;
then  ( Carrier L c= {u} & {u} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31;
then  Carrier L = {u} by XBOOLE_0:def_10;
hence  ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A3, FINSEQ_1:38, FINSEQ_3:93; ::_thesis: verum
end;
hence  L is circled ; ::_thesis: verum
end;
end;

definition
let V be RealLinearSpace;
let M be non empty Subset of V;
mode circled_Combination of M is circled Linear_Combination of M;
end;

definition
let V be RealLinearSpace;
defpred S1[ set ] means $1 is circled_Combination of V;
func circledComb V ->  set  means :: CIRCLED1:def 5
 for L being set holds
( L in it iff L is circled_Combination of V );
existence
 ex b1 being set st
for L being set holds
( L in b1 iff L is circled_Combination of V )
proof
consider A being set  such that
A1: for x being set holds
( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
take  A ; ::_thesis: for L being set holds
( L in A iff L is circled_Combination of V )
let L be set ; ::_thesis: ( L in A iff L is circled_Combination of V )
thus  ( L in A implies L is circled_Combination of V ) by A1; ::_thesis: ( L is circled_Combination of V implies L in A )
assume  L is circled_Combination of V ; ::_thesis: L in A
hence  L in A by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for L being set holds
( L in b1 iff L is circled_Combination of V ) ) & ( for L being set holds
( L in b2 iff L is circled_Combination of V ) ) holds
b1 = b2
proof
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem  defines circledComb CIRCLED1:def_5_:_
 for V being RealLinearSpace
for b2 being set holds
( b2 = circledComb V iff for L being set holds
( L in b2 iff L is circled_Combination of V ) );

definition
let V be RealLinearSpace;
let M be non empty Subset of V;
defpred S1[ set ] means $1 is circled_Combination of M;
func circledComb M ->  set  means :: CIRCLED1:def 6
 for L being set holds
( L in it iff L is circled_Combination of M );
existence
 ex b1 being set st
for L being set holds
( L in b1 iff L is circled_Combination of M )
proof
consider A being set  such that
A1: for x being set holds
( x in A iff ( x in Funcs ( the carrier of V,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
take  A ; ::_thesis: for L being set holds
( L in A iff L is circled_Combination of M )
let L be set ; ::_thesis: ( L in A iff L is circled_Combination of M )
thus  ( L in A implies L is circled_Combination of M ) by A1; ::_thesis: ( L is circled_Combination of M implies L in A )
assume  L is circled_Combination of M ; ::_thesis: L in A
hence  L in A by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for L being set holds
( L in b1 iff L is circled_Combination of M ) ) & ( for L being set holds
( L in b2 iff L is circled_Combination of M ) ) holds
b1 = b2
proof
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem  defines circledComb CIRCLED1:def_6_:_
 for V being RealLinearSpace
for M being non empty Subset of V
for b3 being set holds
( b3 = circledComb M iff for L being set holds
( L in b3 iff L is circled_Combination of M ) );

theorem :: CIRCLED1:19
for V being RealLinearSpace
for v being VECTOR of V ex L being circled_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) )
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V ex L being circled_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) )
let v be VECTOR of V; ::_thesis: ex L being circled_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) )
consider L being Linear_Combination of {v} such that
A1: L . v = 1 by RLVECT_4:37;
consider F being FinSequence of the carrier of V such that
A2: ( F is one-to-one & rng F = Carrier L ) and
 Sum L = Sum (L (#) F) by RLVECT_2:def_8;
 v in Carrier L by A1, RLVECT_2:19;
then  ( Carrier L c= {v} & {v} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:31;
then A3: {v} = Carrier L by XBOOLE_0:def_10;
then  F = <*v*> by A2, FINSEQ_3:97;
then A4: F . 1 = v by FINSEQ_1:def_8;
deffunc H1( set ) ->  set = L . (F . $1);
consider f being FinSequence such that
A5: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H1(n) ) ) from FINSEQ_1:sch_2();
A6: len F = 1 by A3, A2, FINSEQ_3:96;
then  1 in dom f by A5, FINSEQ_3:25;
then A7: f . 1 = L . (F . 1) by A5;
then  f = <*1*> by A1, A5, A6, A4, FINSEQ_1:40;
then reconsider f = f as FinSequence of REAL ;
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A9: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then  n in Seg (len f) by FINSEQ_1:def_3;
hence  ( f . n = L . (F . n) & f . n >= 0 ) by A1, A5, A6, A7, A4, A9, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum
end;
 f = <*1*> by A1, A5, A6, A7, A4, FINSEQ_1:40;
then  Sum f = 1 by FINSOP_1:11;
then reconsider L = L as circled_Combination of V by A2, A5, A8, Def4;
A10: for A being non empty Subset of V st v in A holds
L is circled_Combination of A
proof
let A be non empty Subset of V; ::_thesis: ( v in A implies L is circled_Combination of A )
assume  v in A ; ::_thesis: L is circled_Combination of A
then  {v} c= A by ZFMISC_1:31;
hence  L is circled_Combination of A by A3, RLVECT_2:def_6; ::_thesis: verum
end;
take  L ; ::_thesis: ( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) )
 Sum L = 1 * v by A1, A3, RLVECT_2:35;
hence  ( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) ) by A10, RLVECT_1:def_8; ::_thesis: verum
end;

theorem :: CIRCLED1:20
for V being RealLinearSpace
for v1, v2 being VECTOR of V st v1 <> v2 holds
ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds
ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A
let v1, v2 be VECTOR of V; ::_thesis: ( v1 <> v2 implies ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A )
assume A1: v1 <> v2 ; ::_thesis: ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A
consider L being Linear_Combination of {v1,v2} such that
A2: ( L . v1 = 1 / 2 & L . v2 = 1 / 2 ) by A1, RLVECT_4:38;
consider F being FinSequence of the carrier of V such that
A3: ( F is one-to-one & rng F = Carrier L ) and
 Sum L = Sum (L (#) F) by RLVECT_2:def_8;
deffunc H1( set ) ->  set = L . (F . $1);
consider f being FinSequence such that
A4: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H1(n) ) ) from FINSEQ_1:sch_2();
 ( v1 in Carrier L & v2 in Carrier L ) by A2, RLVECT_2:19;
then  ( Carrier L c= {v1,v2} & {v1,v2} c= Carrier L ) by RLVECT_2:def_6, ZFMISC_1:32;
then A5: {v1,v2} = Carrier L by XBOOLE_0:def_10;
then A6: len F = 2 by A1, A3, FINSEQ_3:98;
then  2 in dom f by A4, FINSEQ_3:25;
then A7: f . 2 = L . (F . 2) by A4;
 1 in dom f by A4, A6, FINSEQ_3:25;
then A8: f . 1 = L . (F . 1) by A4;
now__::_thesis:_ex_L,_L_being_circled_Combination_of_V_st_
for_A_being_non_empty_Subset_of_V_st_{v1,v2}_c=_A_holds_
L_is_circled_Combination_of_A
percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A5, A3, FINSEQ_3:99;
suppose F = <*v1,v2*> ; ::_thesis: ex L, L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A
then A9: ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:44;
then  f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44;
then  f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9;
then  rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31
.= {(1 / 2)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A10: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A11: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then  n in Seg (len f) by FINSEQ_1:def_3;
hence  ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A9, A11, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum
end;
 f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A9, FINSEQ_1:44;
then  Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77
.= 1 ;
then reconsider L = L as circled_Combination of V by A3, A4, A10, Def4;
take L = L; ::_thesis: ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A
 for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A by A5, RLVECT_2:def_6;
hence  ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A ; ::_thesis: verum
end;
suppose F = <*v2,v1*> ; ::_thesis: ex L, L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A
then A12: ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44;
then  f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44;
then  f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def_9;
then  rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:31
.= {(1 / 2)} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def_4;
A13: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
proof
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A14: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then  n in Seg (len f) by FINSEQ_1:def_3;
hence  ( f . n = L . (F . n) & f . n >= 0 ) by A2, A4, A6, A8, A7, A12, A14, FINSEQ_1:2, TARSKI:def_2; ::_thesis: verum
end;
 f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A12, FINSEQ_1:44;
then  Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77
.= 1 ;
then reconsider L = L as circled_Combination of V by A3, A4, A13, Def4;
take L = L; ::_thesis: ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A
 for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A by A5, RLVECT_2:def_6;
hence  ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A ; ::_thesis: verum
end;
end;
end;
hence  ex L being circled_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is circled_Combination of A ; ::_thesis: verum
end;

theorem :: CIRCLED1:21
for V being RealLinearSpace
for L1, L2 being circled_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being circled_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let L1, L2 be circled_Combination of V; ::_thesis: for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
let a, b be Real; ::_thesis: ( a * b > 0 implies Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) )
assume  a * b > 0 ; ::_thesis: Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
then A1: ( not ( a >= 0 & b <= 0 ) & not ( a <= 0 & b >= 0 ) ) ;
then A2: Carrier L2 = Carrier (b * L2) by RLVECT_2:42;
A3: Carrier L1 = Carrier (a * L1) by A1, RLVECT_2:42;
 for x being set st x in (Carrier (a * L1)) \/ (Carrier (b * L2)) holds
x in Carrier ((a * L1) + (b * L2))
proof
let x be set ; ::_thesis: ( x in (Carrier (a * L1)) \/ (Carrier (b * L2)) implies x in Carrier ((a * L1) + (b * L2)) )
assume A4: x in (Carrier (a * L1)) \/ (Carrier (b * L2)) ; ::_thesis: x in Carrier ((a * L1) + (b * L2))
percases ( x in Carrier (a * L1) or x in Carrier (b * L2) ) by A4, XBOOLE_0:def_3;
supposeA5: x in Carrier (a * L1) ; ::_thesis: x in Carrier ((a * L1) + (b * L2))
then  x in  {  v where v is Element of V : (a * L1) . v <> 0  }  by RLVECT_2:def_4;
then consider v being Element of V such that
A6: v = x and
A7: (a * L1) . v <> 0 ;
A8: L1 . v > 0 by A3, A5, A6, Th17;
 v in Carrier ((a * L1) + (b * L2))
proof
percases ( v in Carrier L2 or not v in Carrier L2 ) ;
supposeA9: v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then A10: L2 . v > 0 by Th17;
percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;
supposeA11: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then  b * (L2 . v) > 0 by A10, XREAL_1:129;
then  (b * L2) . v > 0 by RLVECT_2:def_11;
then A12: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29;
 a * (L1 . v) > 0 by A8, A11, XREAL_1:129;
then  (a * L1) . v > 0 by RLVECT_2:def_11;
then  ((a * L1) + (b * L2)) . v > 0 by A12, RLVECT_2:def_10;
hence  v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
supposeA13: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then  a * (L1 . v) < 0 by A3, A5, A6, Th17, XREAL_1:132;
then  (a * L1) . v < 0 by RLVECT_2:def_11;
then A14: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30;
 b * (L2 . v) < 0 by A9, A13, Th17, XREAL_1:132;
then  (b * L2) . v < 0 by RLVECT_2:def_11;
then  ((a * L1) + (b * L2)) . v < 0 by A14, RLVECT_2:def_10;
hence  v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
suppose not v in Carrier L2 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then  L2 . v = 0 by RLVECT_2:19;
then  b * (L2 . v) = 0 ;
then  (b * L2) . v = 0 by RLVECT_2:def_11;
then  ((a * L1) . v) + ((b * L2) . v) = (a * L1) . v ;
then  ((a * L1) + (b * L2)) . v <> 0 by A7, RLVECT_2:def_10;
hence  v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
hence  x in Carrier ((a * L1) + (b * L2)) by A6; ::_thesis: verum
end;
supposeA15: x in Carrier (b * L2) ; ::_thesis: x in Carrier ((a * L1) + (b * L2))
then  x in  {  v where v is Element of V : (b * L2) . v <> 0  }  by RLVECT_2:def_4;
then consider v being Element of V such that
A16: v = x and
A17: (b * L2) . v <> 0 ;
A18: L2 . v > 0 by A2, A15, A16, Th17;
 v in Carrier ((a * L1) + (b * L2))
proof
percases ( v in Carrier L1 or not v in Carrier L1 ) ;
supposeA19: v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then A20: L1 . v > 0 by Th17;
percases ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1;
supposeA21: ( a > 0 & b > 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then  b * (L2 . v) > 0 by A18, XREAL_1:129;
then  (b * L2) . v > 0 by RLVECT_2:def_11;
then A22: ((a * L1) . v) + ((b * L2) . v) > (a * L1) . v by XREAL_1:29;
 a * (L1 . v) > 0 by A20, A21, XREAL_1:129;
then  (a * L1) . v > 0 by RLVECT_2:def_11;
then  ((a * L1) + (b * L2)) . v > 0 by A22, RLVECT_2:def_10;
hence  v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
supposeA23: ( a < 0 & b < 0 ) ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then  a * (L1 . v) < 0 by A19, Th17, XREAL_1:132;
then  (a * L1) . v < 0 by RLVECT_2:def_11;
then A24: ((a * L1) . v) + ((b * L2) . v) < (b * L2) . v by XREAL_1:30;
 b * (L2 . v) < 0 by A2, A15, A16, A23, Th17, XREAL_1:132;
then  (b * L2) . v < 0 by RLVECT_2:def_11;
then  ((a * L1) + (b * L2)) . v < 0 by A24, RLVECT_2:def_10;
hence  v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
suppose not v in Carrier L1 ; ::_thesis: v in Carrier ((a * L1) + (b * L2))
then  L1 . v = 0 by RLVECT_2:19;
then  a * (L1 . v) = 0 ;
then  (a * L1) . v = 0 by RLVECT_2:def_11;
then  ((a * L1) . v) + ((b * L2) . v) = (b * L2) . v ;
then  ((a * L1) + (b * L2)) . v <> 0 by A17, RLVECT_2:def_10;
hence  v in Carrier ((a * L1) + (b * L2)) by RLVECT_2:19; ::_thesis: verum
end;
end;
end;
hence  x in Carrier ((a * L1) + (b * L2)) by A16; ::_thesis: verum
end;
end;
end;
then A25: (Carrier (a * L1)) \/ (Carrier (b * L2)) c= Carrier ((a * L1) + (b * L2)) by TARSKI:def_3;
 Carrier ((a * L1) + (b * L2)) c= (Carrier (a * L1)) \/ (Carrier (b * L2)) by RLVECT_2:37;
hence  Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by A25, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th22: :: CIRCLED1:22
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is circled & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for L being Linear_Combination of V st L is circled & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )
let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V st L is circled & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )
let L be Linear_Combination of V; ::_thesis: ( L is circled & Carrier L = {v} implies ( L . v = 1 & Sum L = (L . v) * v ) )
assume that
A1: L is circled and
A2: Carrier L = {v} ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v )
reconsider L = L as Linear_Combination of {v} by A2, RLVECT_2:def_6;
consider F being FinSequence of the carrier of V such that
A3: ( F is one-to-one & rng F = Carrier L ) and
A4: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4;
A5: F = <*v*> by A2, A3, FINSEQ_3:97;
consider f being FinSequence of REAL  such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A4;
reconsider r = f /. 1 as Element of REAL ;
 card (Carrier L) = 1 by A2, CARD_1:30;
then  len F = 1 by A3, FINSEQ_4:62;
then A9: dom f = Seg 1 by A6, FINSEQ_1:def_3;
then A10: 1 in dom f by FINSEQ_1:2, TARSKI:def_1;
then A11: f . 1 = f /. 1 by PARTFUN1:def_6;
then  f = <*r*> by A9, FINSEQ_1:def_8;
then A12: Sum f = r by FINSOP_1:11;
 f . 1 = L . (F . 1) by A8, A10;
hence  ( L . v = 1 & Sum L = (L . v) * v ) by A7, A11, A12, A5, FINSEQ_1:def_8, RLVECT_2:32; ::_thesis: verum
end;

theorem Th23: :: CIRCLED1:23
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let v1, v2 be VECTOR of V; ::_thesis: for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let L be Linear_Combination of V; ::_thesis: ( L is circled & Carrier L = {v1,v2} & v1 <> v2 implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) )
assume that
A1: L is circled and
A2: Carrier L = {v1,v2} and
A3: v1 <> v2 ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
reconsider L = L as Linear_Combination of {v1,v2} by A2, RLVECT_2:def_6;
consider F being FinSequence of the carrier of V such that
A4: ( F is one-to-one & rng F = Carrier L ) and
A5: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1, Def4;
consider f being FinSequence of REAL  such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A5;
 len F = card {v1,v2} by A2, A4, FINSEQ_4:62;
then A9: len f = 2 by A3, A6, CARD_2:57;
then A10: dom f = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
then A11: 1 in dom f by TARSKI:def_2;
then A12: f . 1 = L . (F . 1) by A8;
then  f /. 1 = L . (F . 1) by A11, PARTFUN1:def_6;
then reconsider r1 = L . (F . 1) as Element of REAL ;
A13: 2 in dom f by A10, TARSKI:def_2;
then A14: f . 2 = L . (F . 2) by A8;
then  f /. 2 = L . (F . 2) by A13, PARTFUN1:def_6;
then reconsider r2 = L . (F . 2) as Element of REAL ;
A15: f = <*r1,r2*> by A9, A12, A14, FINSEQ_1:44;
now__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_)
percases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A2, A3, A4, FINSEQ_3:99;
suppose F = <*v1,v2*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
then  ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:44;
hence  ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A7, A8, A11, A13, A12, A14, A15, RVSUM_1:77; ::_thesis: verum
end;
suppose F = <*v2,v1*> ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
then  ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44;
hence  ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A7, A8, A11, A13, A12, A14, A15, RVSUM_1:77; ::_thesis: verum
end;
end;
end;
hence  ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A3, RLVECT_2:33; ::_thesis: verum
end;

theorem :: CIRCLED1:24
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of {v} st L is circled holds
( L . v = 1 & Sum L = (L . v) * v )
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for L being Linear_Combination of {v} st L is circled holds
( L . v = 1 & Sum L = (L . v) * v )
let v be VECTOR of V; ::_thesis: for L being Linear_Combination of {v} st L is circled holds
( L . v = 1 & Sum L = (L . v) * v )
let L be Linear_Combination of {v}; ::_thesis: ( L is circled implies ( L . v = 1 & Sum L = (L . v) * v ) )
 Carrier L c= {v} by RLVECT_2:def_6;
then A1: ( Carrier L = {} or Carrier L = {v} ) by ZFMISC_1:33;
assume  L is circled ; ::_thesis: ( L . v = 1 & Sum L = (L . v) * v )
hence  ( L . v = 1 & Sum L = (L . v) * v ) by A1, Th16, Th22; ::_thesis: verum
end;

theorem :: CIRCLED1:25
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proof
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for L being Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let v1, v2 be VECTOR of V; ::_thesis: for L being Linear_Combination of {v1,v2} st v1 <> v2 & L is circled holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let L be Linear_Combination of {v1,v2}; ::_thesis: ( v1 <> v2 & L is circled implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) )
assume that
A1: v1 <> v2 and
A2: L is circled ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
A3: ( Carrier L c= {v1,v2} & Carrier L <> {} ) by A2, Th16, RLVECT_2:def_6;
now__::_thesis:_(_(L_._v1)_+_(L_._v2)_=_1_&_L_._v1_>=_0_&_L_._v2_>=_0_)
percases ( Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v1,v2} ) by A3, ZFMISC_1:36;
supposeA4: Carrier L = {v1} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
then  not v2 in Carrier L by A1, TARSKI:def_1;
then  not v2 in  {  v where v is Element of V : L . v <> 0  }  by RLVECT_2:def_4;
then  L . v2 = 0 ;
hence  ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A2, A4, Th22; ::_thesis: verum
end;
supposeA5: Carrier L = {v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
then  not v1 in Carrier L by A1, TARSKI:def_1;
then  not v1 in  {  v where v is Element of V : L . v <> 0  }  by RLVECT_2:def_4;
then  L . v1 = 0 ;
hence  ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A2, A5, Th22; ::_thesis: verum
end;
suppose Carrier L = {v1,v2} ; ::_thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 )
hence  ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A1, A2, Th23; ::_thesis: verum
end;
end;
end;
hence  ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A1, RLVECT_2:33; ::_thesis: verum
end;