CONVEX4

:: Convex Sets and Convex Combinations on Complex Linear Spaces
::  by Hidenori Matsuzaki , Noboru Endou and Yasunari Shidama
::
:: Received March 3, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, STRUCT_0, SUBSET_1, FUNCT_2, FINSET_1,
      FUNCT_1, CARD_1, FUNCOP_1, COMPLEX1, ALGSTR_0, RLVECT_2, TARSKI, NAT_1,
      CLVECT_1, FINSEQ_1, VALUED_1, RELAT_1, PARTFUN1, XXREAL_0, RLVECT_1,
      CARD_3, SUPINF_2, RLSUB_1, ARYTM_3, ARYTM_1, QC_LANG1, BINOP_1, ZFMISC_1,
      RUSUB_4, REAL_1, REALSET1, XCMPLX_0, CONVEX1, SETFAM_1, CSSPACE, PROB_2,
      CONVEX4, PRE_POLY, FUNCT_7;
 notations TARSKI, XBOOLE_0, ENUMSET1, DOMAIN_1, ZFMISC_1, SUBSET_1, RELAT_1,
      FUNCT_1, PRE_POLY, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_4, ALGSTR_0,
      RLVECT_1, SETFAM_1, STRUCT_0, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
      FINSET_1, PARTFUN1, FUNCOP_1, CARD_1, VALUED_1, XCMPLX_0, COMPLEX1,
      RVSUM_1, RUSUB_4, RUSUB_5, BINOP_1, REAL_1, RLVECT_2, CLVECT_1, CSSPACE,
      REALSET1;
 constructors SETFAM_1, BINOP_1, FUNCOP_1, REAL_1, FINSEQ_4, COMPLEX1,
      REALSET1, BINOP_2, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5, CSSPACE,
      RELSET_1;
 registrations STRUCT_0, MEMBERED, XXREAL_0, CSSPACE, RLVECT_1, RELSET_1,
      FINSET_1, XREAL_0, SUBSET_1, XCMPLX_0, CLVECT_1, NUMBERS, NAT_1, FUNCT_2,
      VALUED_1, VALUED_0, CARD_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions FUNCT_1, TARSKI, XBOOLE_0, ALGSTR_0;
 equalities XBOOLE_0, BINOP_1, RELAT_1, STRUCT_0, REALSET1, FINSEQ_1, CLVECT_1,
      COMPLEX1, RVSUM_1, XCMPLX_0, ALGSTR_0, RUSUB_4, RUSUB_5;
 expansions TARSKI, BINOP_1, STRUCT_0, CLVECT_1, ALGSTR_0;
 theorems RVSUM_1, SETFAM_1, ENUMSET1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_3,
      FINSEQ_4, FUNCT_1, FUNCT_2, NAT_1, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1,
      RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, COMPLEX1, XCMPLX_1, FUNCOP_1,
      XREAL_1, XXREAL_0, FINSOP_1, CLVECT_1, CSSPACE, CONVEX1, PARTFUN1,
      XREAL_0, VALUED_1, ALGSTR_0, PRE_POLY, XCMPLX_0;
 schemes DOMAIN_1, BINOP_1, SUBSET_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0;

begin :: Complex Linear Combinations

definition
  let V be non empty 1-sorted;
  mode C_Linear_Combination of V -> Element of Funcs(the carrier of V, COMPLEX)
  means
    :Def1:
    ex T being finite Subset of V st for v being Element of V st not v in T
    holds it.v = 0;
  existence
  proof
    reconsider f = (the carrier of V) --> 0c as
    Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:8;
    take f,{}V;
    thus thesis by FUNCOP_1:7;
  end;
end;

notation
  let V be non empty addLoopStr,
      L be Element of Funcs(the carrier of V,COMPLEX);
  synonym Carrier L for support L;
end;

Lm1: now
  let V be non empty addLoopStr,
      L be Element of Funcs(the carrier of V, COMPLEX);
A1: support L c= dom L by PRE_POLY:37;
  thus Carrier L c= the carrier of V
  proof
    let x be object;
    assume x in support L;
    then x in dom L by A1;
    hence thesis;
  end;
end;

definition
  let V be non empty addLoopStr,
      L be Element of Funcs(the carrier of V,COMPLEX);
  redefine func Carrier L -> Subset of V equals  :: redefines Carrier (CONVEX4, synonym) → support (PRE_POLY, definition)
  {v where v is Element of V : L.v <> 0c};
  coherence by Lm1;
  compatibility
  proof
    let X be Subset of V;
    set A = Carrier L;
    set B = {v where v is Element of V : L.v <> 0};
    thus X = A implies X = B
    proof
      assume
A1:   X = A;
      thus X c= B
      proof
        let x be object;
        assume
A2:     x in X;
        then L.x <> 0 by A1,PRE_POLY:def 7;
        hence thesis by A2;
      end;
      let x be object;
      assume x in B;
      then ex v be Element of V st x = v & L.v <> 0;
      hence thesis by A1,PRE_POLY:def 7;
    end;
    assume
A3: X = B;
    thus X c= A
    proof
      let x be object;
      assume x in X;
      then ex v be Element of V st x = v & L.v <> 0 by A3;
      hence thesis by PRE_POLY:def 7;
    end;
    let x be object;
    assume
A4: x in A;
    then
A5: L.x <> 0 by PRE_POLY:def 7;
    Carrier L c= the carrier of V by Lm1;
    hence thesis by A3,A4,A5;
  end;
end;

registration
  let V be non empty addLoopStr, L be C_Linear_Combination of V;
  cluster Carrier L -> finite;
  coherence
  proof
    set A = Carrier L;
    consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds L.v = 0c by Def1;
    now
      let x be object;
      assume x in A;
      then ex v being Element of V st x = v & L.v <> 0c;
      hence x in T by A1;
    end;
    then A c= T;
    hence thesis;
  end;
end;

theorem Th1:
  for V be non empty addLoopStr, L be C_Linear_Combination of V, v
  be Element of V holds L.v = 0c iff not v in Carrier L
proof
  let V be non empty addLoopStr, L be C_Linear_Combination of V, v be Element
  of V;
  thus L.v = 0c implies not v in Carrier L
  proof
    assume
A1: L.v = 0c;
    assume not thesis;
    then ex u being Element of V st v=u & L.u <> 0c;
    hence thesis by A1;
  end;
  thus thesis;
end;

definition
  let V be non empty addLoopStr;
  func ZeroCLC V -> C_Linear_Combination of V means
  :Def3:
  Carrier it = {};
  existence
  proof
    reconsider f = (the carrier of V) --> 0c as
    Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:8;
    f is C_Linear_Combination of V
    proof
      take {}V;
      thus thesis by FUNCOP_1:7;
    end;
    then reconsider f as C_Linear_Combination of V;
    take f;
    set C = {v where v is Element of V : f.v <> 0c};
    now
      set x = the Element of C;
      assume C <> {};
      then x in C;
      then ex v being Element of V st x = v & f.v <> 0c;
      hence contradiction by FUNCOP_1:7;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let L,L9 be C_Linear_Combination of V;
    assume
A1: Carrier L = {} & Carrier L9 = {};
    now
      let x be object;
      assume x in the carrier of V;
      then reconsider v = x as Element of V;
A2:   L9.v <> 0c implies v in {u where u is Element of V : L9.u <> 0c};
      L.v <> 0c implies v in {u where u is Element of V : L.u <> 0c};
      hence L.x = L9.x by A1,A2;
    end;
    hence L = L9 by FUNCT_2:12;
  end;
end;

registration
  let V be non empty addLoopStr;
  cluster Carrier ZeroCLC V -> empty;
  coherence by Def3;
end;

theorem Th2:
  for V be non empty addLoopStr, v be Element of V holds (ZeroCLC V ).v = 0c
proof
  let V be non empty addLoopStr, v be Element of V;
  Carrier (ZeroCLC V) = {} & not v in {};
  hence thesis;
end;

definition
  let V be non empty addLoopStr;
  let A be Subset of V;
  mode C_Linear_Combination of A -> C_Linear_Combination of V means
    :Def4:
    Carrier it c= A;
  existence
  proof
    take L = ZeroCLC V;
    thus thesis;
  end;
end;

theorem
  for V be non empty addLoopStr, A,B be Subset of V, l be
  C_Linear_Combination of A st A c= B holds l is C_Linear_Combination of B
proof
  let V be non empty addLoopStr;
  let A,B be Subset of V;
  let l be C_Linear_Combination of A;
  assume
A1: A c= B;
  Carrier l c= A by Def4;
  then Carrier l c= B by A1;
  hence thesis by Def4;
end;

theorem Th4:
  for V be non empty addLoopStr, A be Subset of V holds ZeroCLC V
  is C_Linear_Combination of A
proof
  let V be non empty addLoopStr;
  let A be Subset of V;
  Carrier ZeroCLC V = {} & {} c= A;
  hence thesis by Def4;
end;

theorem Th5:
  for V being non empty addLoopStr, l being C_Linear_Combination of
  {}the carrier of V holds l = ZeroCLC V
proof
  let V be non empty addLoopStr;
  let l be C_Linear_Combination of {}(the carrier of V);
  Carrier l c= {} by Def4;
  then Carrier l = {};
  hence thesis by Def3;
end;

reserve x,y for set,
  i for Nat;

definition
  let V be non empty CLSStruct;
  let F be FinSequence of the carrier of V;
  let f be Function of the carrier of V,COMPLEX;
  func f (#) F -> FinSequence of the carrier of V means
  :Def5:
  len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i;
  existence
  proof
    deffunc Q(set)= f.(F/.$1) * F/.$1;
    consider G being FinSequence such that
A1: len G = len F and
A2: for n be Nat st n in dom G holds G.n = Q(n) from FINSEQ_1:sch 2;
    rng G c= the carrier of V
    proof
      let x be object;
      assume x in rng G;
      then consider y being object such that
A3:   y in dom G and
A4:   G.y = x by FUNCT_1:def 3;
      reconsider y as Element of NAT by A3;
      G.y = f.(F/.y) * F/.y by A2,A3;
      hence thesis by A4;
    end;
    then reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4;
    take G;
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let H1,H2 be FinSequence of the carrier of V;
    assume that
A5: len H1 = len F and
A6: for i st i in dom H1 holds H1.i = f.(F/.i) * F/.i and
A7: len H2 = len F and
A8: for i st i in dom H2 holds H2.i = f.(F/.i) * F/.i;
    now
      let k be Nat;
      assume 1 <= k & k <= len H1;
      then
A9:   k in Seg len H1;
      then k in dom H1 by FINSEQ_1:def 3;
      then
A10:  H1.k = f.(F/.k) * F/.k by A6;
      k in dom H2 by A5,A7,A9,FINSEQ_1:def 3;
      hence H1.k = H2.k by A8,A10;
    end;
    hence thesis by A5,A7,FINSEQ_1:14;
  end;
end;

reserve V for non empty CLSStruct,
  u,v,v1,v2,v3 for VECTOR of V,
  A for Subset of V,
  l, l1, l2 for C_Linear_Combination of A,
  x,y,y1,y2 for set,
  a,b for Complex,
  F for FinSequence of the carrier of V,
  f for Function of the carrier of V, COMPLEX;

theorem Th6:
  x in dom F & v = F.x implies (f (#) F).x = f.v * v
proof
  assume that
A1: x in dom F and
A2: v = F.x;
A3: F/.x = F.x by A1,PARTFUN1:def 6;
  len(f (#) F) = len F by Def5;
  then x in dom(f (#) F) by A1,FINSEQ_3:29;
  hence thesis by A2,A3,Def5;
end;

theorem
  f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
  len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def5
    .= 0;
  hence thesis;
end;

theorem Th8:
  f (#) <* v *> = <* f.v * v *>
proof
A1: 1 in {1} by FINSEQ_1:2;
A2: len(f (#) <* v *>) = len<* v *> by Def5
    .= 1 by FINSEQ_1:40;
  then dom(f (#)<* v *>) = {1} by FINSEQ_1:2,def 3;
  then (f (#) <* v *>).1 = f.(<* v *>/.1) * <* v *>/.1 by A1,Def5
    .= f.(<* v *>/.1) * v by FINSEQ_4:16
    .= f.v * v by FINSEQ_4:16;
  hence thesis by A2,FINSEQ_1:40;
end;

theorem Th9:
  f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def5
    .= 2 by FINSEQ_1:44;
  then
A2: dom(f (#) <* v1,v2 *>) = {1,2} by FINSEQ_1:2,def 3;
  2 in {1,2} by FINSEQ_1:2;
  then
A3: (f (#) <* v1,v2 *>).2 = f.(<* v1,v2 *>/.2) * <* v1,v2 *>/.2 by A2,Def5
    .= f.(<* v1,v2 *>/.2) * v2 by FINSEQ_4:17
    .= f.v2 * v2 by FINSEQ_4:17;
  1 in {1,2} by FINSEQ_1:2;
  then (f (#) <* v1,v2 *>).1 = f.(<* v1,v2 *>/.1) * <* v1,v2 *>/.1 by A2,Def5
    .= f.(<* v1,v2 *>/.1) * v1 by FINSEQ_4:17
    .= f.v1 * v1 by FINSEQ_4:17;
  hence thesis by A1,A3,FINSEQ_1:44;
end;

theorem Th10:
  f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>
proof
A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by Def5
    .= 3 by FINSEQ_1:45;
  then
A2: dom(f (#)<* v1,v2,v3 *>) = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
  3 in {1,2,3} by FINSEQ_3:1;
  then
A3: (f (#) <* v1,v2,v3 *>).3 = f.(<* v1,v2,v3 *>/.3) * <* v1,v2,v3 *>/.3 by A2
,Def5
    .= f.(<* v1,v2,v3 *>/.3) * v3 by FINSEQ_4:18
    .= f.v3 * v3 by FINSEQ_4:18;
  2 in {1,2,3} by FINSEQ_3:1;
  then
A4: (f (#) <* v1,v2,v3 *>).2 = f.(<* v1,v2,v3 *>/.2) * <* v1,v2,v3 *>/.2 by A2
,Def5
    .= f.(<* v1,v2,v3 *>/.2) * v2 by FINSEQ_4:18
    .= f.v2 * v2 by FINSEQ_4:18;
  1 in {1,2,3} by FINSEQ_3:1;
  then
  (f (#) <* v1,v2,v3 *>).1 = f.(<* v1,v2,v3 *>/.1) * <* v1,v2,v3 *>/.1 by A2
,Def5
    .= f.(<* v1,v2,v3 *>/.1) * v1 by FINSEQ_4:18
    .= f.v1 * v1 by FINSEQ_4:18;
  hence thesis by A1,A4,A3,FINSEQ_1:45;
end;

reserve K,L,L1,L2,L3 for C_Linear_Combination of V;

definition
  let V be Abelian add-associative right_zeroed right_complementable non empty
  CLSStruct;
  let L be C_Linear_Combination of V;
  func Sum L -> Element of V means
  :Def6:
  ex F being FinSequence of the
  carrier of V st F is one-to-one & rng F = Carrier L & it = Sum(L (#) F);
  existence
  proof
    consider F being FinSequence such that
A1: rng F = Carrier L and
A2: F is one-to-one by FINSEQ_4:58;
    reconsider F as FinSequence of the carrier of V by A1,FINSEQ_1:def 4;
    take Sum(L (#) F);
    take F;
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let v1,v2 be Element of V;
    given F1 being FinSequence of the carrier of V such that
A3: F1 is one-to-one and
A4: rng F1 = Carrier L and
A5: v1 = Sum(L (#) F1);
    given F2 being FinSequence of the carrier of V such that
A6: F2 is one-to-one and
A7: rng F2 = Carrier L and
A8: v2 = Sum(L (#) F2);
    defpred P[object,object] means {$2} = F1"{F2.$1};
A9: len F1 = len F2 by A3,A4,A6,A7,FINSEQ_1:48;
A10: dom F1 = Seg len F1 by FINSEQ_1:def 3;
A11: dom F2 = Seg len F2 by FINSEQ_1:def 3;
A12: for x being object st x in dom F1
ex y being object st y in dom F1 & P[x,y]
    proof
      let x be object;
      assume x in dom F1;
      then F2.x in rng F1 by A4,A7,A9,A10,A11,FUNCT_1:def 3;
      then consider y being object such that
A13:  F1"{F2.x} = {y} by A3,FUNCT_1:74;
      take y;
      y in F1"{F2.x} by A13,TARSKI:def 1;
      hence thesis by A13,FUNCT_1:def 7;
    end;
    consider f being Function of dom F1, dom F1 such that
A14: for x being object st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A12);
A15: rng f = dom F1
    proof
      thus rng f c= dom F1 by RELAT_1:def 19;
      let y be object;
      assume
A16:  y in dom F1;
      then F1.y in rng F2 by A4,A7,FUNCT_1:def 3;
      then consider x being object such that
A17:  x in dom F2 and
A18:  F2.x = F1.y by FUNCT_1:def 3;
      F1"{F2.x} = F1"Im(F1,y) by A16,A18,FUNCT_1:59;
      then F1"{F2.x} c= {y} by A3,FUNCT_1:82;
      then {f.x} c= {y} by A9,A10,A11,A14,A17;
      then
A19:  f.x = y by ZFMISC_1:18;
      x in dom f by A9,A10,A11,A17,FUNCT_2:def 1;
      hence thesis by A19,FUNCT_1:def 3;
    end;
    set G1 = L (#) F1;
A20: len G1 = len F1 by Def5;
A21: f is one-to-one
    proof
      let y1,y2 be object;
      assume that
A22:  y1 in dom f and
A23:  y2 in dom f and
A24:  f.y1 = f.y2;
      F2.y1 in rng F1 by A4,A7,A9,A10,A11,A22,FUNCT_1:def 3;
      then
A25:  {F2.y1} c= rng F1 by ZFMISC_1:31;
      F2.y2 in rng F1 by A4,A7,A9,A10,A11,A23,FUNCT_1:def 3;
      then
A26:  {F2.y2} c= rng F1 by ZFMISC_1:31;
      F1"{F2.y1} = {f.y1} & F1"{F2.y2} = {f.y2} by A14,A22,A23;
      then {F2.y1} = {F2.y2} by A24,A25,A26,FUNCT_1:91;
      then F2.y1 = F2.y2 by ZFMISC_1:3;
      hence thesis by A6,A9,A10,A11,A22,A23,FUNCT_1:def 4;
    end;
    set G2 = L (#) F2;
A27: dom G2 = Seg len G2 by FINSEQ_1:def 3;
    reconsider f as Permutation of dom F1 by A15,A21,FUNCT_2:57;
    dom F1 = Seg len F1 & dom G1 = Seg len G1 by FINSEQ_1:def 3;
    then reconsider f as Permutation of dom G1 by A20;
A28: len G2 = len F2 by Def5;
A29: dom G1 = Seg len G1 by FINSEQ_1:def 3;
    now
      let i be Nat;
      assume
A30:  i in dom G2;
      then
A31:  G2.i = L.(F2/.i) * F2/.i & F2.i = F2/.i by A28,A11,A27,Def5,
PARTFUN1:def 6;
      i in dom f by A9,A28,A10,A27,A30,FUNCT_2:def 1;
      then
A32:  f.i in dom F1 by A15,FUNCT_1:def 3;
      then reconsider m = f.i as Element of NAT;
      {F1.(f.i)} = Im(F1,f.i) by A32,FUNCT_1:59
        .= F1.:(F1"{F2.i}) by A9,A28,A10,A27,A14,A30;
      then
A33:  F2.i = F1.m by FUNCT_1:75,ZFMISC_1:18;
      F1.m = F1/.m by A32,PARTFUN1:def 6;
      hence G2.i = G1.(f.i) by A20,A10,A29,A32,A33,A31,Def5;
    end;
    hence thesis by A3,A4,A5,A6,A7,A8,A20,A28,FINSEQ_1:48,RLVECT_2:6;
  end;
end;

theorem Th11:
  for V being Abelian add-associative right_zeroed
  right_complementable non empty CLSStruct holds Sum(ZeroCLC V) = 0.V
proof
  let V be Abelian add-associative right_zeroed right_complementable non empty
  CLSStruct;
  consider F being FinSequence of the carrier of V such that
  F is one-to-one and
A1: rng F = Carrier (ZeroCLC V) and
A2: Sum(ZeroCLC V) = Sum(ZeroCLC V (#) F) by Def6;
  F = {} by A1,RELAT_1:41;
  then len(ZeroCLC V (#) F) = 0 by Def5,CARD_1:27;
  hence thesis by A2,RLVECT_1:75;
end;

theorem
  for V being ComplexLinearSpace, A being Subset of V holds A <> {}
implies ( A is linearly-closed iff for l being C_Linear_Combination of A holds
  Sum l in A )
proof
  let V be ComplexLinearSpace;
  let A be Subset of V;
  assume
A1: A <> {};
  thus A is linearly-closed implies for l being C_Linear_Combination of A
  holds Sum l in A
  proof
    defpred P[Nat] means for l being C_Linear_Combination of A st card(Carrier
    l) = $1 holds Sum l in A;
    assume
A2: A is linearly-closed;
A3: for k be Nat st P[k] holds P[k+1]
    proof
      let k be Nat;
      assume
A4:   P[k];
      hereby
        let l be C_Linear_Combination of A;
        deffunc F(Element of V)= l.$1;
        consider F being FinSequence of the carrier of V such that
A5:     F is one-to-one and
A6:     rng F = Carrier l and
A7:     Sum l = Sum(l (#) F) by Def6;
        reconsider G = F | Seg k as FinSequence of the carrier of V by
FINSEQ_1:18;
        assume
A8:     card(Carrier l) = k + 1;
        then
A9:     len F = k + 1 by A5,A6,FINSEQ_4:62;
        then
A10:    len(l (#) F) = k + 1 by Def5;
        k + 1 in Seg(k + 1) by FINSEQ_1:4;
        then
A11:    k + 1 in dom F by A9,FINSEQ_1:def 3;
        then reconsider v = F.(k + 1) as VECTOR of V by FUNCT_1:102;
        consider f being Function of the carrier of V, COMPLEX such that
A12:    f.v = 0c & for u being Element of V st u <> v holds f.u = F(u
        ) from FUNCT_2:sch 6;
        reconsider f as Element of Funcs(the carrier of V, COMPLEX) by
FUNCT_2:8;
        now
          let u be VECTOR of V;
          assume not u in Carrier l;
          then l.u = 0c;
          hence f.u = 0c by A12;
        end;
        then reconsider f as C_Linear_Combination of V by Def1;
A13:    Carrier f = Carrier l \ {v}
        proof
          now
            let x be object;
            assume x in Carrier f;
            then
A14:        ex u being VECTOR of V st u = x & f.u <> 0c;
            then f.x = l.x by A12;
            then
A15:        x in Carrier l by A14;
            not x in {v} by A12,A14,TARSKI:def 1;
            hence x in Carrier l \ {v} by A15,XBOOLE_0:def 5;
          end;
          hence Carrier f c= Carrier l \ {v};
          let x be object;
          assume
A16:      x in Carrier l \ {v};
          then not x in {v} by XBOOLE_0:def 5;
          then x <> v by TARSKI:def 1;
          then
A17:      l.x = f.x by A12,A16;
          x in Carrier l by A16,XBOOLE_0:def 5;
          then ex u being VECTOR of V st x = u & l.u <> 0c;
          hence thesis by A17;
        end;
A18:    Carrier l c= A by Def4;
        then Carrier f c= A \ {v} by A13,XBOOLE_1:33;
        then Carrier f c= A by XBOOLE_1:106;
        then reconsider f as C_Linear_Combination of A by Def4;
A19:    len G = k by A9,FINSEQ_3:53;
        then
A20:    len (f (#) G) = k by Def5;
A21:    rng G = Carrier f
        proof
          thus rng G c= Carrier f
          proof
            let x be object;
            assume x in rng G;
            then consider y being object such that
A22:        y in dom G and
A23:        G.y = x by FUNCT_1:def 3;
            reconsider y as Element of NAT by A22;
A24:        dom G c= dom F & G.y = F.y by A22,FUNCT_1:47,RELAT_1:60;
            then x = v implies k + 1 = y & y <= k & k < k + 1 by A5,A19,A11,A22
,A23,FINSEQ_3:25,FUNCT_1:def 4,XREAL_1:29;
            then
A25:        not x in {v} by TARSKI:def 1;
            x in rng F by A22,A23,A24,FUNCT_1:def 3;
            hence thesis by A6,A13,A25,XBOOLE_0:def 5;
          end;
          let x be object;
          assume
A26:      x in Carrier f;
          then x in rng F by A6,A13,XBOOLE_0:def 5;
          then consider y being object such that
A27:      y in dom F and
A28:      F.y = x by FUNCT_1:def 3;
          now
            assume not y in Seg k;
            then y in dom F \ Seg k by A27,XBOOLE_0:def 5;
            then y in Seg(k + 1) \ Seg k by A9,FINSEQ_1:def 3;
            then y in {k + 1} by FINSEQ_3:15;
            then y = k + 1 by TARSKI:def 1;
            then not v in {v} by A13,A26,A28,XBOOLE_0:def 5;
            hence contradiction by TARSKI:def 1;
          end;
          then y in dom F /\ Seg k by A27,XBOOLE_0:def 4;
          then
A29:      y in dom G by RELAT_1:61;
          then G.y = F.y by FUNCT_1:47;
          hence thesis by A28,A29,FUNCT_1:def 3;
        end;
        Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:7,NAT_1:12
          .= dom(f (#) G) by A20,FINSEQ_1:def 3;
        then
A30:    dom(f (#) G) = dom(l (#) F) /\ Seg k by A10,FINSEQ_1:def 3;
        now
          let x be object;
          assume
A31:      x in dom(f (#) G);
          then
A32:      x in dom G by A19,A20,FINSEQ_3:29;
          then
A33:      G.x in rng G by FUNCT_1:def 3;
          then reconsider u = G.x as VECTOR of V;
A34:      F.x = u by A32,FUNCT_1:47;
          not u in {v} by A13,A21,A33,XBOOLE_0:def 5;
          then
A35:      u <> v by TARSKI:def 1;
          x in dom(l (#) F) by A30,A31,XBOOLE_0:def 4;
          then
A36:      x in dom F by A9,A10,FINSEQ_3:29;
          (f (#) G).x = f.u * u by A32,Th6
            .= l.u * u by A12,A35;
          hence (f (#) G).x = (l (#) F).x by A36,A34,Th6;
        end;
        then
A37:    f (#) G = (l (#) F) | Seg k by A30,FUNCT_1:46;
        v in rng F by A11,FUNCT_1:def 3;
        then {v} c= Carrier l by A6,ZFMISC_1:31;
        then card(Carrier f) = k + 1 - card{v} by A8,A13,CARD_2:44;
        then card(Carrier f) = k + 1 - 1 by CARD_1:30;
        then
A38:    Sum f in A by A4;
        v in Carrier l by A6,A11,FUNCT_1:def 3;
        then
A39:    l.v * v in A by A2,A18;
        G is one-to-one by A5,FUNCT_1:52;
        then
A40:    Sum(f (#) G) = Sum f by A21,Def6;
        dom(f (#) G) = Seg len (f (#) G) & (l (#) F).(len F) = l.v * v by A9
,A11,Th6,FINSEQ_1:def 3;
        then Sum(l (#) F) = Sum(f (#) G) + l.v * v by A9,A10,A20,A37,
RLVECT_1:38;
        hence Sum l in A by A2,A7,A39,A40,A38;
      end;
    end;
    let l be C_Linear_Combination of A;
A41: card(Carrier l) = card(Carrier l);
    now
      let l be C_Linear_Combination of A;
      assume card(Carrier l) = 0;
      then Carrier l = {};
      then l = ZeroCLC V by Def3;
      then Sum l = 0.V by Th11;
      hence Sum l in A by A1,A2,CLVECT_1:20;
    end;
    then
A42: P[0];
    for k be Nat holds P[k] from NAT_1:sch 2(A42,A3);
    hence thesis by A41;
  end;
  assume
A43: for l be C_Linear_Combination of A holds Sum l in A;
  ZeroCLC V is C_Linear_Combination of A & Sum(ZeroCLC V) = 0.V by Th4,Th11;
  then
A44: 0.V in A by A43;
A45: for a being Complex,v being VECTOR of V st v in A holds a * v in A
  proof
    let a be Complex, v be VECTOR of V;
    assume
A46: v in A;
    now
      reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
      deffunc F(Element of V) = 0c;
      consider f being Function of the carrier of V, COMPLEX such that
A47:  f.v = a1 & for u being Element of V st u <> v holds f.u = F(u)
      from FUNCT_2:sch 6;
      reconsider f as Element of Funcs(the carrier of V,COMPLEX) by FUNCT_2:8;
      now
        let u be VECTOR of V;
        assume not u in {v};
        then u <> v by TARSKI:def 1;
        hence f.u = 0 by A47;
      end;
      then reconsider f as C_Linear_Combination of V by Def1;
      assume
A48:  a <> 0;
A49:  Carrier f = {v}
      proof
        now
          let x be object;
          assume x in Carrier f;
          then ex u being VECTOR of V st x = u & f.u <> 0;
          then x = v by A47;
          hence x in {v} by TARSKI:def 1;
        end;
        hence Carrier f c= {v};
        let x be object;
        assume x in {v};
        then x = v by TARSKI:def 1;
        hence thesis by A48,A47;
      end;
      {v} c= A by A46,ZFMISC_1:31;
      then reconsider f as C_Linear_Combination of A by A49,Def4;
      consider F being FinSequence of the carrier of V such that
A50:  F is one-to-one & rng F = Carrier f and
A51:  Sum(f(#)F) = Sum f by Def6;
      F = <* v *> by A49,A50,FINSEQ_3:97;
      then f (#) F = <* f.v * v *> by Th8;
      then Sum f = a * v by A47,A51,RLVECT_1:44;
      hence thesis by A43;
    end;
    hence thesis by A44,CLVECT_1:1;
  end;
  for v,u being VECTOR of V st v in A & u in A holds v + u in A
  proof
    let v,u be VECTOR of V;
    assume that
A52: v in A and
A53: u in A;
A54: 1r * v = v by CLVECT_1:def 5;
A55: 1r * u = u by CLVECT_1:def 5;
A56: now
      deffunc F(Element of V)=0c;
      assume
A57:  v <> u;
      consider f being Function of the carrier of V, COMPLEX such that
A58:  f.v = 1r & f.u = 1r and
A59:  for w being Element of V st w <> v & w <> u holds f.w = F(w)
      from FUNCT_2:sch 7(A57);
      reconsider f as Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:8;
      now
        let w be VECTOR of V;
        assume not w in {v,u};
        then w <> v & w <> u by TARSKI:def 2;
        hence f.w = 0 by A59;
      end;
      then reconsider f as C_Linear_Combination of V by Def1;
A60:  Carrier f = {v,u}
      proof
        thus Carrier f c= {v,u}
        proof
          let x be object;
          assume x in Carrier f;
          then ex w being VECTOR of V st x = w & f.w <> 0c;
          then x = v or x = u by A59;
          hence thesis by TARSKI:def 2;
        end;
        let x be object;
        assume x in {v,u};
        then x = v or x = u by TARSKI:def 2;
        hence thesis by A58;
      end;
      then Carrier f c= A by A52,A53,ZFMISC_1:32;
      then reconsider f as C_Linear_Combination of A by Def4;
      consider F being FinSequence of the carrier of V such that
A61:  F is one-to-one & rng F = Carrier f and
A62:  Sum(f (#) F) = Sum f by Def6;
      F = <* v,u *> or F = <* u,v *> by A57,A60,A61,FINSEQ_3:99;
      then f(#)F = <* 1r*v, 1r*u *> or f(#)F = <* 1r*u, 1r*v *> by A58,Th9;
      then Sum f = v + u by A55,A54,A62,RLVECT_1:45;
      hence thesis by A43;
    end;
    v + v = (1r + 1r) * v by A54,CLVECT_1:def 3;
    hence thesis by A45,A52,A56;
  end;
  hence thesis by A45;
end;

theorem
  for V being Abelian add-associative right_zeroed right_complementable
non empty CLSStruct, l being C_Linear_Combination of {}(the carrier of V) holds
  Sum l = 0.V
proof
  let V be Abelian add-associative right_zeroed right_complementable non empty
  CLSStruct;
  let l be C_Linear_Combination of {}(the carrier of V);
  l = ZeroCLC V by Th5;
  hence thesis by Th11;
end;

theorem Th14:
  for V being ComplexLinearSpace, v being VECTOR of V, l being
  C_Linear_Combination of {v} holds Sum l = l.v * v
proof
  let V be ComplexLinearSpace;
  let v be VECTOR of V;
  let l be C_Linear_Combination of {v};
A1: Carrier l c= {v} by Def4;
  per cases by A1,ZFMISC_1:33;
  suppose
    Carrier l = {};
    then
A2: l = ZeroCLC V by Def3;
    hence Sum l = 0.V by Th11
      .= 0c * v by CLVECT_1:1
      .= l.v * v by A2,Th2;
  end;
  suppose
    Carrier l = {v};
    then consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = {v} and
A4: Sum l = Sum(l (#) F) by Def6;
    F = <* v *> by A3,FINSEQ_3:97;
    then l (#) F = <* l.v * v *> by Th8;
    hence thesis by A4,RLVECT_1:44;
  end;
end;

theorem Th15:
  for V being ComplexLinearSpace, v1, v2 being VECTOR of V holds
v1 <> v2 implies for l being C_Linear_Combination of {v1,v2} holds Sum l = l.v1
  * v1 + l.v2 * v2
proof
  let V be ComplexLinearSpace;
  let v1, v2 be VECTOR of V;
  assume
A1: v1 <> v2;
  let l be C_Linear_Combination of {v1,v2};
A2: 0.V = 0c*v1 by CLVECT_1:1;
A3: Carrier l c= {v1,v2} by Def4;
A4: 0.V = 0c*v2 by CLVECT_1:1;
  per cases by A3,ZFMISC_1:36;
  suppose
    Carrier l = {};
    then
A5: l = ZeroCLC V by Def3;
    hence Sum l = 0.V by Th11
      .= 0.V + 0.V
      .= l.v1 * v1 + 0c* v2 by A4,A5,Th2,CLVECT_1:1
      .= l.v1 * v1 + l.v2 * v2 by A5,Th2;
  end;
  suppose
A6: Carrier l = {v1};
    then reconsider L = l as C_Linear_Combination of {v1} by Def4;
    Sum L = l.v1 * v1 by Th14;
    then
A7: Sum l = l.v1 * v1 + 0.V;
    not v2 in Carrier l by A1,A6,TARSKI:def 1;
    hence thesis by A4,A7;
  end;
  suppose
A8: Carrier l = {v2};
    then reconsider L = l as C_Linear_Combination of {v2} by Def4;
    Sum L = l.v2 * v2 by Th14;
    then
A9: Sum l = 0.V + l.v2 * v2;
    not v1 in Carrier l by A1,A8,TARSKI:def 1;
    hence thesis by A2,A9;
  end;
  suppose
    Carrier l = {v1,v2};
    then consider F being FinSequence of the carrier of V such that
A10: F is one-to-one & rng F = {v1,v2} and
A11: Sum l = Sum(l (#) F) by Def6;
    F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A10,FINSEQ_3:99;
    then l (#) F = <* l.v1 * v1, l.v2 * v2 *> or l (#) F = <* l.v2 * v2, l.v1
    * v1 *> by Th9;
    hence thesis by A11,RLVECT_1:45;
  end;
end;

theorem
  for V being Abelian add-associative right_zeroed right_complementable
  non empty CLSStruct, L being C_Linear_Combination of V holds Carrier L = {}
  implies Sum L = 0.V
proof
  let V be Abelian add-associative right_zeroed right_complementable non empty
  CLSStruct;
  let L be C_Linear_Combination of V;
  assume Carrier L = {};
  then L = ZeroCLC V by Def3;
  hence thesis by Th11;
end;

theorem
  for V being ComplexLinearSpace, L being C_Linear_Combination of V, v
  being VECTOR of V holds Carrier L = {v} implies Sum L = L.v * v
proof
  let V be ComplexLinearSpace;
  let L be C_Linear_Combination of V;
  let v be VECTOR of V;
  assume Carrier L = {v};
  then L is C_Linear_Combination of {v} by Def4;
  hence thesis by Th14;
end;

theorem Th18:
  for V being ComplexLinearSpace, L being C_Linear_Combination of
V, v1, v2 being VECTOR of V holds Carrier L = {v1,v2} & v1 <> v2 implies Sum L
  = L.v1 * v1 + L.v2 * v2
proof
  let V be ComplexLinearSpace;
  let L be C_Linear_Combination of V;
  let v1, v2 be VECTOR of V;
  assume that
A1: Carrier L = {v1,v2} and
A2: v1 <> v2;
  L is C_Linear_Combination of {v1,v2} by A1,Def4;
  hence thesis by A2,Th15;
end;

definition
  let V be non empty addLoopStr;
  let L1,L2 be C_Linear_Combination of V;
  redefine pred L1 = L2 means  :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
  for v being Element of V holds L1.v = L2.v;
  compatibility by FUNCT_2:63;
end;

definition
  let V be non empty addLoopStr;
  let L1,L2 be C_Linear_Combination of V;
  redefine func L1 + L2 -> C_Linear_Combination of V means  :: redefines + (VALUED_1, definition)
  :Def8:
  for v being Element of V holds it.v = L1.v + L2.v;
  coherence
  proof
    reconsider f = L1+L2 as Element of Funcs(the carrier of V,COMPLEX) by
FUNCT_2:8;
    now
      let v be Element of V;
      assume
A1:   not v in Carrier(L1) \/ Carrier(L2);
      then not v in Carrier(L2) by XBOOLE_0:def 3;
      then
A2:   L2.v = 0;
      not v in Carrier(L1) by A1,XBOOLE_0:def 3;
      then L1.v = 0;
      hence f.v = 0 + 0 by A2,VALUED_1:1
        .= 0;
    end;
    hence thesis by Def1;
  end;
  compatibility
  proof
    let f be C_Linear_Combination of V;
    thus f=L1+L2 implies for v being Element of V holds f.v = L1.v + L2.v by
VALUED_1:1;
    assume for v being Element of V holds f.v = L1.v + L2.v;
    then
A3: for c being object st c in dom f holds f.c = L1.c + L2.c;
    dom L1 = the carrier of V & dom L2 = the carrier of V by FUNCT_2:92;
    then dom f = dom L1 /\ dom L2 by FUNCT_2:92;
    hence f=L1+L2 by A3,VALUED_1:def 1;
  end;
end;

theorem Th19:
  Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2
proof
  let x be object;
  assume x in Carrier(L1 + L2);
  then consider u such that
A1: x = u and
A2: (L1 + L2).u <> 0c;
  (L1 + L2).u = L1.u + L2.u by Def8;
  then L1.u <> 0c or L2.u <> 0c by A2;
  then x in Carrier L1 or x in Carrier L2 by A1;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th20:
  L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of
  A implies L1 + L2 is C_Linear_Combination of A
proof
  assume L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A;
  then Carrier L1 c= A & Carrier L2 c= A by Def4;
  then
A1: Carrier L1 \/ Carrier L2 c= A by XBOOLE_1:8;
  Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2 by Th19;
  hence Carrier(L1 + L2) c= A by A1;
end;

definition
  let V,A;
  let L1,L2 be C_Linear_Combination of A;
  redefine func L1 + L2 -> C_Linear_Combination of A;  :: redefines + (VALUED_1, definition)
  coherence by Th20;
end;

theorem
  for V be non empty addLoopStr, L1,L2 be C_Linear_Combination of V
  holds L1 + L2 = L2 + L1;

theorem Th22:
  L1 + (L2 + L3) = L1 + L2 + L3
proof
  let v;
  thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Def8
    .= L1.v + (L2.v + L3.v) by Def8
    .= L1.v + L2.v + L3.v
    .= (L1 + L2).v + L3.v by Def8
    .= (L1 + L2 + L3).v by Def8;
end;

theorem Th23:
  L + ZeroCLC V = L
proof
  let v;
  thus (L + ZeroCLC V).v = L.v + (ZeroCLC V).v by Def8
    .= L.v + 0c by Th2
    .= L.v;
end;

definition
  let V; let a be Complex;
  let L;
  func a * L -> C_Linear_Combination of V means
  :Def9:
  for v holds it.v = a * L.v;
  existence
  proof
    reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
    deffunc F(Element of V)=In(a * L.$1,COMPLEX);
    consider f being Function of the carrier of V, COMPLEX such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
    reconsider f as Element of Funcs(the carrier of V,COMPLEX) by FUNCT_2:8;
    now
      let v;
      assume not v in Carrier L;
      then
A2:    L.v = 0c;
      thus f.v = F(v) by A1
        .= 0c by A2;
    end;
    then reconsider f as C_Linear_Combination of V by Def1;
    take f;
    let v;
     f.v = F(v) by A1;
    hence thesis;
  end;
  uniqueness
  proof
    let L1,L2;
    assume
A3: for v holds L1.v = a * L.v;
    assume
A4: for v holds L2.v = a * L.v;
    let v;
    thus L1.v = a * L.v by A3
      .= L2.v by A4;
  end;
end;

theorem Th24:
  a <> 0c implies Carrier (a * L) = Carrier L
proof
  set T = {u : (a * L).u <> 0c};
  set S = {v : L.v <> 0c};
  assume
A1: a <> 0c;
  T = S
  proof
    thus T c= S
    proof
      let x be object;
      assume x in T;
      then consider u such that
A2:   x = u and
A3:   (a * L).u <> 0c;
      (a * L).u = a * L.u by Def9;
      then L.u <> 0c by A3;
      hence thesis by A2;
    end;
    let x be object;
    assume x in S;
    then consider v such that
A4: x = v & L.v <> 0c;
    (a * L).v = a * L.v by Def9;
    hence thesis by A1,A4;
  end;
  hence thesis;
end;

theorem Th25:
  0c * L = ZeroCLC V
proof
  let v;
  thus (0c * L).v = 0c * L.v by Def9
    .= (ZeroCLC V).v by Th2;
end;

theorem Th26:
  L is C_Linear_Combination of A implies a * L is C_Linear_Combination of A
proof
  assume
A1: L is C_Linear_Combination of A;
A2: now
    assume a <> 0c;
    then Carrier (a * L) = Carrier L by Th24;
    hence thesis by A1,Def4;
  end;
  a = 0c implies a*L = ZeroCLC V by Th25;
  hence thesis by A2,Th4;
end;

theorem Th27:
  (a + b) * L = a * L + b * L
proof
  let v;
  thus ((a + b) * L).v = (a + b) * L.v by Def9
    .= a * L.v + b * L.v
    .= (a * L).v + b * L.v by Def9
    .= (a * L).v + (b * L). v by Def9
    .= ((a * L) + (b * L)).v by Def8;
end;

theorem Th28:
  a * (L1 + L2) = a * L1 + a * L2
proof
  let v;
  thus (a * (L1 + L2)).v = a * (L1 + L2).v by Def9
    .= a * (L1.v + L2.v) by Def8
    .= a * L1.v + a * L2.v
    .= (a * L1).v + a * L2.v by Def9
    .= (a * L1).v + (a * L2). v by Def9
    .= ((a * L1) + (a * L2)).v by Def8;
end;

theorem Th29:
  a * (b * L) = (a * b) * L
proof
  let v;
  thus (a * (b * L)).v = a * (b * L).v by Def9
    .= a * (b * L.v) by Def9
    .= a * b * L.v
    .= ((a * b) * L).v by Def9;
end;

theorem Th30:
  1r * L = L
proof
  let v;
  thus (1r * L).v = 1r * L.v by Def9
    .= L.v;
end;

definition
  let V,L;
  func - L -> C_Linear_Combination of V equals
  (- 1r) * L;
  correctness;
end;

theorem Th31:
  (- L).v = - L.v
proof
  thus (- L).v = (- 1r) * L.v by Def9
    .= - L.v;
end;

theorem
  L1 + L2 = ZeroCLC V implies L2 = - L1
proof
  assume
A1: L1 + L2 = ZeroCLC V;
  let v;
  L1.v + L2.v = (ZeroCLC V).v by A1,Def8
    .= 0c by Th2;
  hence L2.v = - L1.v .= (- L1).v by Th31;
end;

theorem
  - (- L) = L
proof
  let v;
  thus (- (- L)).v = ((- 1r) * (- 1r) * L).v by Th29
    .= 1r * L.v by Def9
    .= L.v;
end;

definition
  let V;
  let L1,L2;
  func L1 - L2 -> C_Linear_Combination of V equals
  L1 + (- L2);
  correctness;
end;

theorem Th34:
  (L1 - L2).v = L1.v - L2.v
proof
  thus (L1 - L2).v = L1.v + (- L2).v by Def8
    .= L1.v - L2.v by Th31;
end;

theorem
  Carrier(L1 - L2) c= Carrier L1 \/ Carrier L2
proof
  Carrier(L1 - L2) c= Carrier L1 \/ Carrier -L2 by Th19;
  hence thesis by Th24;
end;

theorem
  L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A
  implies L1 - L2 is C_Linear_Combination of A
proof
  assume that
A1: L1 is C_Linear_Combination of A and
A2: L2 is C_Linear_Combination of A;
  - L2 is C_Linear_Combination of A by A2,Th26;
  hence thesis by A1,Th20;
end;

theorem Th37:
  L - L = ZeroCLC V
proof
  let v;
  thus (L - L).v = L.v - L.v by Th34
    .= (ZeroCLC V).v by Th2;
end;

definition
  let V;
  func C_LinComb V -> set means
  :Def12:
  x in it iff x is C_Linear_Combination of V;
  existence
  proof
    defpred P[object] means $1 is C_Linear_Combination of V;
    consider A being set such that
A1: for x being object
holds x in A iff x in Funcs(the carrier of V, COMPLEX) & P[x
    ] from XBOOLE_0:sch 1;
    take A;
    let x;
    thus x in A implies x is C_Linear_Combination of V by A1;
    assume x is C_Linear_Combination of V;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let D1,D2 be set;
    assume
A2: for x holds x in D1 iff x is C_Linear_Combination of V;
    assume
A3: for x holds x in D2 iff x is C_Linear_Combination of V;
    thus D1 c= D2
    proof
      let x be object;
      assume x in D1;
      then x is C_Linear_Combination of V by A2;
      hence thesis by A3;
    end;
    let x be object;
    assume x in D2;
    then x is C_Linear_Combination of V by A3;
    hence thesis by A2;
  end;
end;

registration
  let V;
  cluster C_LinComb V -> non empty;
  coherence
  proof
    set x = the C_Linear_Combination of V;
    x in C_LinComb V by Def12;
    hence thesis;
  end;
end;

reserve e,e1,e2 for Element of C_LinComb V;

definition
  let V;
  let e;
  func @e -> C_Linear_Combination of V equals
  e;
  coherence by Def12;
end;

definition
  let V;
  let L;
  func @L -> Element of C_LinComb V equals
  L;
  coherence by Def12;
end;

definition
  let V;
  func C_LCAdd V -> BinOp of C_LinComb V means
  :Def15:
  for e1,e2 holds it.(e1, e2) = @e1 + @e2;
  existence
  proof
    deffunc F(Element of C_LinComb V,Element of C_LinComb V)=@(@$1 + @$2);
    consider o being BinOp of C_LinComb V such that
A1: for e1,e2 holds o.(e1,e2) = F(e1,e2) from BINOP_1:sch 4;
    take o;
    let e1,e2;
    thus o.(e1,e2) = @(@e1 + @e2) by A1
      .= @e1 + @e2;
  end;
  uniqueness
  proof
    let o1,o2 be BinOp of C_LinComb V;
    assume
A2: for e1,e2 holds o1.(e1,e2) = @e1 + @e2;
    assume
A3: for e1,e2 holds o2.(e1,e2) = @e1 + @e2;
    now
      let e1,e2;
      thus o1.(e1,e2) = @e1 + @e2 by A2
        .= o2.(e1,e2) by A3;
    end;
    hence thesis;
  end;
end;

definition
  let V;
  func C_LCMult V -> Function of [:COMPLEX,C_LinComb V:], C_LinComb V means
  :Def16: for a,e holds it.[a,e] = a * @e;
  existence
  proof
    defpred P[Element of COMPLEX,Element of C_LinComb V,set] means ex a st a =
    $1 & $3 = a * @$2;
A1: for x being (Element of COMPLEX), e1 ex e2 st P[x,e1,e2]
    proof
      let x be (Element of COMPLEX), e1;
      take @(x * @e1);
      take x;
      thus thesis;
    end;
    consider g being Function of [:COMPLEX,C_LinComb V:], C_LinComb V such
    that
A2: for x being Element of COMPLEX, e holds P[x,e,g.(x,e)] from
    BINOP_1:sch 3(A1);
    take g;
    let a,e;
    a in COMPLEX by XCMPLX_0:def 2;
    then ex b st b = a & g.(a,e) = b * @e by A2;
    hence thesis;
  end;
  uniqueness
  proof
    let g1,g2 be Function of [:COMPLEX,C_LinComb V:], C_LinComb V;
    assume
A3: for a,e holds g1.[a,e] = a * @e;
    assume
A4: for a,e holds g2.[a,e] = a * @e;
    now
      let x be (Element of COMPLEX), e;
      thus g1.(x,e) = x * @e by A3
        .= g2.(x,e) by A4;
    end;
    hence thesis;
  end;
end;

definition
  let V;
  func LC_CLSpace V -> ComplexLinearSpace equals
  CLSStruct (# C_LinComb V, @
    ZeroCLC V, C_LCAdd V, C_LCMult V #);
  coherence
  proof
    set S = CLSStruct (# C_LinComb V, @ZeroCLC V, C_LCAdd V, C_LCMult V #);
A1: now
      let a,b be Complex, v,u,w be VECTOR of S;
      reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;
      reconsider x = v, y = u, z = w, yx = u + v, xz = v + w, ax = a1 * v, az =
      a1 * w, bx = b1 * v as Element of C_LinComb V;
A2:   @z = w & @yx = u + v;
A3:   @xz = v + w & @ax = a * v;
A4:   @az = a * w & @bx = b * v;
      @x = v & @y = u;
      then reconsider
      K = v, L = u, M = w, LK = u + v, KM = v + w, aK = a * v, aM =
      a * w, bK = b * v as C_Linear_Combination of V by A2,A3,A4;
A5:   now
        let v,u be (VECTOR of S), K,L;
A6:     @@K = K & @@L = L;
        assume v = K & u = L;
        hence v + u = K + L by A6,Def15;
      end;
      hence v + w = K + M .= w + v by A5;
      thus (u + v) + w = LK + M by A5
        .= L + K + M by A5
        .= L + (K + M) by Th22
        .= L + KM by A5
        .= u + (v + w) by A5;
      thus v + 0.S = K + ZeroCLC V by A5
        .= v by Th23;
      - K in the carrier of S by Def12;
      then - K in S;
      then - K = vector(S,- K) by RLVECT_2:def 1;
      then v + vector(S,- K) = K - K by A5
        .= 0.S by Th37;
      hence ex w being VECTOR of S st v + w = 0.S;
A7:   now
        let v be (VECTOR of S), L; let a be Complex;
        assume v = L;
        then (C_LCMult V).[a,v] = a*@@L by Def16;
        hence a*v = a*L;
      end;
      hence a * (v + w) = a1 * KM .= a1 * (K + M) by A5
        .= a1 * K + a1 * M by Th28
        .= aK + a1 * M by A7
        .= aK + aM by A7
        .= a * v + a * w by A5;
      thus (a + b) * v = (a1 + b1) * K by A7
        .= a1 * K + b1 * K by Th27
        .= aK + b * K by A7
        .= aK + bK by A7
        .= a * v + b * v by A5;
      thus (a * b) * v = (a * b) * K by A7
        .= a1 * (b1 * K) by Th29
        .= a * (bK) by A7
        .= a * (b * v) by A7;
      thus 1r * v = 1r * K by A7
        .= v by Th30;
    end;
A8: for v be Element of S holds v is right_complementable by A1;
    for u,v,w being VECTOR of S holds (u + v) + w = u + (v + w) by A1;
    hence thesis by A1,A8,ALGSTR_0:def 16,CLVECT_1:def 2,def 3,def 4,def 5
,RLVECT_1:def 2,def 3,def 4;
  end;
end;

registration
  let V;
  cluster LC_CLSpace V -> strict non empty;
  coherence;
end;

theorem Th38:
  vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2) = L1 + L2
proof
  set v2 = vector(LC_CLSpace V,L2);
A1: L1 = @@L1 & L2 = @@L2;
  L2 in the carrier of LC_CLSpace V by Def12;
  then
A2: L2 in LC_CLSpace V;
  L1 in the carrier of LC_CLSpace V by Def12;
  then L1 in LC_CLSpace V;
  hence
  vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2) = (C_LCAdd V).[L1,v2]
  by RLVECT_2:def 1
    .= (C_LCAdd V).(@L1,@L2) by A2,RLVECT_2:def 1
    .= L1 + L2 by A1,Def15;
end;

theorem Th39:
  a * vector(LC_CLSpace V,L) = a * L
proof
  L in the carrier of LC_CLSpace V by Def12;
  then L in LC_CLSpace V;
  then
A1: (C_LCMult V).[a,vector(LC_CLSpace V,L)] = (C_LCMult V).[a,@L] by
RLVECT_2:def 1;
  @@L = L;
  hence thesis by A1,Def16;
end;

theorem Th40:
  - vector(LC_CLSpace V,L) = - L
proof
  thus - vector(LC_CLSpace V,L) = (- 1r) * (vector(LC_CLSpace V,L)) by
CLVECT_1:3
    .= - L by Th39;
end;

theorem
  vector(LC_CLSpace V,L1) - vector(LC_CLSpace V,L2) = L1 - L2
proof
  - L2 in C_LinComb V by Def12;
  then
A1: - L2 in LC_CLSpace V;
  - vector(LC_CLSpace V,L2) = - L2 by Th40
    .= vector(LC_CLSpace V,- L2) by A1,RLVECT_2:def 1;
  hence thesis by Th38;
end;

definition
  let V;
  let A;
  func LC_CLSpace A -> strict Subspace of LC_CLSpace V means
  the carrier of it = the set of all l ;
  existence
  proof
    set X = the set of all l ;
    X c= the carrier of LC_CLSpace V
    proof
      let x be object;
      assume x in X;
      then ex l st x = l;
      hence thesis by Def12;
    end;
    then reconsider X as Subset of LC_CLSpace V;
A1: for v,u being VECTOR of LC_CLSpace V st v in X & u in X holds v + u in X
    proof
      let v,u be VECTOR of LC_CLSpace V;
      assume that
A2:   v in X and
A3:   u in X;
      consider l1 such that
A4:   v = l1 by A2;
      consider l2 such that
A5:   u = l2 by A3;
A6:   u = vector(LC_CLSpace V,l2) by A5,RLVECT_2:1;
      v = vector(LC_CLSpace V,l1) by A4,RLVECT_2:1;
      then v + u = l1 + l2 by A6,Th38;
      hence thesis;
    end;
    ZeroCLC V is C_Linear_Combination of A by Th4;
    then
A7: ZeroCLC V in X;
    for a being Complex, v being VECTOR of LC_CLSpace V st v in X holds a
    *v in X
    proof
      let a be Complex;
      let v be VECTOR of LC_CLSpace V;
      assume v in X;
      then consider l such that
A8:   v = l;
      a * v = a * vector(LC_CLSpace V,l) by A8,RLVECT_2:1
        .= a * l by Th39;
      then a * v is C_Linear_Combination of A by Th26;
      hence thesis;
    end;
    then X is linearly-closed by A1;
    hence thesis by A7,CLVECT_1:54;
  end;
  uniqueness by CLVECT_1:49;
end;

begin :: Preliminaries for Complex Convex Sets

definition
  let V be ComplexLinearSpace, W be Subspace of V;
  func Up W -> Subset of V equals
  the carrier of W;
  coherence by CLVECT_1:def 8;
end;

registration
  let V be ComplexLinearSpace, W be Subspace of V;
  cluster Up W -> non empty;
  coherence;
end;

definition
  let V be non empty CLSStruct, S be Subset of V;
  attr S is Affine means

  for x,y being VECTOR of V, z being Complex st
  z is Real & x in S & y in S holds (1r - z) * x + z * y in S;
end;

definition
  let V be ComplexLinearSpace;
  func (Omega).V -> strict Subspace of V equals
  the CLSStruct of V;
  coherence
  proof
    set W = the CLSStruct of V;
A1: for v,w being VECTOR of W holds v + w = w + v
    proof
      let v,w be VECTOR of W;
      reconsider v9=v,w9=w as VECTOR of V;
      v+w = v9+w9;
      hence v + w = w9 + v9 .= w + v;
    end;
A2: for u,v,w being VECTOR of W holds (u + v) + w = u + (v + w)
    proof
      let u,v,w be VECTOR of W;
      reconsider u9=u,v9=v,w9=w as VECTOR of V;
      (u9 + v9) + w9 = u9 + (v9 + w9) by RLVECT_1:def 3;
      hence thesis;
    end;
A3: for v being VECTOR of W holds v is right_complementable
    proof
      let v be VECTOR of W;
      reconsider v9 = v as VECTOR of V;
      v9 is right_complementable by ALGSTR_0:def 16;
      then consider w9 being VECTOR of V such that
A4:   v9 + w9 = 0.V;
      reconsider w = w9 as VECTOR of W;
      take w;
      thus thesis by A4;
    end;
A5: for v being VECTOR of W holds v + 0.W = v
    proof
      let v be VECTOR of W;
      reconsider v9=v as VECTOR of V;
      thus v + 0.W = v9 + 0.V .= v;
    end;
A6: for a,b for v being VECTOR of W holds (a * b) * v = a * (b * v)
    proof
      let a,b;
      let v be VECTOR of W;
      reconsider v9=v as VECTOR of V;
      (a * b) * v9 = a * (b * v9) by CLVECT_1:def 4;
      hence thesis;
    end;
A7: for a,b for v being VECTOR of W holds (a + b) * v = a * v + b * v
    proof
      let a,b;
      let v be VECTOR of W;
      reconsider v9=v as VECTOR of V;
      (a + b) * v9 = a * v9 + b * v9 by CLVECT_1:def 3;
      hence thesis;
    end;
A8: for a for v,w being VECTOR of W holds a * (v + w) = a * v + a * w
    proof
      let a;
      let v,w be VECTOR of W;
      reconsider v9=v,w9=w as VECTOR of V;
      a * (v9 + w9) = a * v9 + a * w9 by CLVECT_1:def 2;
      hence thesis;
    end;
    for v being VECTOR of W holds 1r * v = v
    proof
      let v be VECTOR of W;
      reconsider v9=v as VECTOR of V;
      thus 1r * v = 1r * v9 .= v by CLVECT_1:def 5;
    end;
    then reconsider W as ComplexLinearSpace by A1,A2,A5,A3,A8,A7,A6,
ALGSTR_0:def 16,CLVECT_1:def 2,def 3,def 4,def 5,RLVECT_1:def 2,def 3,def 4;
A9: the Mult of W = (the Mult of V) | [:COMPLEX, the carrier of W:] by
RELSET_1:19;
    0.W = 0.V & the addF of W = (the addF of V) || (the carrier of W) by
RELSET_1:19;
    hence thesis by A9,CLVECT_1:def 8;
  end;
end;

registration
  let V be non empty CLSStruct;
  cluster [#]V -> Affine;
  coherence;
  cluster empty -> Affine for Subset of V;
  coherence;
end;

registration
  let V be non empty CLSStruct;
  cluster non empty Affine for Subset of V;
  existence
  proof
    take [#]V;
    thus thesis;
  end;
  cluster empty Affine for Subset of V;
  existence
  proof
    take {}V;
    thus thesis;
  end;
end;

theorem Th42:
  for a being Real, z being Complex holds Re(a*z)=a* Re(z)
proof
  let a be Real;
  let z be Complex;
  Re(a * z) = Re a * Re z - Im a * Im z by COMPLEX1:9
    .= Re a * Re z - 0 * Im z by COMPLEX1:def 2
    .= a * Re (z) by COMPLEX1:def 1;
  hence thesis;
end;

theorem Th43:
  for a being Real, z being Complex holds Im(a*z) = a*Im(z)
proof
  let a be Real;
  let z be Complex;
  Im(a * z) = Re a * Im z + Re z * Im a by COMPLEX1:9
    .= Re a * Im z + Re z * 0 by COMPLEX1:def 2
    .= a * Im (z) by COMPLEX1:def 1;
  hence thesis;
end;

theorem Th44:
  for a being Real , z being Complex st 0<=a & a<=1
  holds |.a*z.| = a*|.z.| & |.(1r-a)*z.| = (1r-a)*|.z.|
proof
  let a be Real;
  let z be Complex;
  assume that
A1: 0<=a and
A2: a<=1;
A3: |.(1r-a)*z.| = |.1r-a.|*|.z.| by COMPLEX1:65
    .= (1r-a)*|.z.| by A2,COMPLEX1:43,XREAL_1:48;
  |.a*z.| = |.a.|*|.z.| by COMPLEX1:65
    .= a * |.z.| by A1,COMPLEX1:43;
  hence thesis by A3;
end;

begin  :: Complex Convex Sets

definition
  let V be non empty CLSStruct;
  let M be Subset of V;
  let r be Complex;
  func r*M -> Subset of V equals
  {r * v where v is Element of V: v in M};
  coherence
  proof
    deffunc F(Element of V) = r * $1;
    defpred P[set] means $1 in M;
    {F(v) where v is Element of V: P[v]} is Subset of V from DOMAIN_1:sch 8;
    hence thesis;
  end;
end;

definition
  let V be non empty CLSStruct;
  let M be Subset of V;
  attr M is convex means

  for u,v being VECTOR of V, z be Complex st
  (ex r be Real st z=r & 0 < r & r < 1 ) & u in M & v in M holds
  z*u + (1r-z)*v in M;
end;

theorem
  for V being vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct, M being
  Subset of V, z being Complex st M is convex holds z*M is convex
proof
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct;
  let M be Subset of V;
  let z be Complex;
  assume
A1: M is convex;
  for u,v being VECTOR of V, s being Complex st (ex p being Real st s=p &
  0 < p & p < 1) & u in z*M & v in z*M holds s*u + (1r-s)*v in z*M
  proof
    let u,v be VECTOR of V;
    let s be Complex;
    assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: u in z*M and
A4: v in z*M;
    consider v9 be Element of V such that
A5: v = z*v9 and
A6: v9 in M by A4;
    consider u9 be Element of V such that
A7: u = z * u9 and
A8: u9 in M by A3;
A9: s*u + (1r-s)*v = s*z*u9 + (1r-s)*(z*v9) by A7,A5,CLVECT_1:def 4
      .= z*s*u9 + z*(1r-s)*v9 by CLVECT_1:def 4
      .= z*(s*u9) + z*(1r-s)*v9 by CLVECT_1:def 4
      .= z*(s*u9) + z*((1r-s)*v9) by CLVECT_1:def 4
      .= z*(s*u9 + (1r-s)*v9) by CLVECT_1:def 2;
    s*u9 + (1r-s)*v9 in M by A1,A2,A8,A6;
    hence thesis by A9;
  end;
  hence thesis;
end;

theorem
  for V being Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty
  CLSStruct, M,N being Subset of V st M is convex & N is convex holds M + N is
  convex
proof
  let V be Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty
  CLSStruct;
  let M,N be Subset of V;
  assume
A1: M is convex & N is convex;
  for u,v being VECTOR of V, z being Complex st (ex r being Real st z=r &
  0 < r & r < 1) & u in M+N & v in M+N holds z*u + (1r-z)*v in M+N
  proof
    let u,v be VECTOR of V;
    let z be Complex;
    assume that
A2: ex r being Real st z=r & 0 < r & r < 1 and
A3: u in M+N and
A4: v in M+N;
    consider x2,y2 being Element of V such that
A5: v = x2 + y2 and
A6: x2 in M & y2 in N by A4;
    consider x1,y1 being Element of V such that
A7: u = x1 + y1 and
A8: x1 in M & y1 in N by A3;
A9: z*u + (1r-z)*v = z*x1 + z*y1 + (1r-z)*(x2+y2) by A7,A5,CLVECT_1:def 2
      .= z*x1 + z*y1 + ((1r-z)*x2 + (1r-z)*y2) by CLVECT_1:def 2
      .= z*x1 + z*y1 + (1r-z)*x2 + (1r-z)*y2 by RLVECT_1:def 3
      .= z*x1 + (1r-z)*x2 + z*y1 + (1r-z)*y2 by RLVECT_1:def 3
      .= (z*x1 + (1r-z)*x2) + (z*y1 + (1r-z)*y2) by RLVECT_1:def 3;
    z*x1 + (1r-z)*x2 in M & z*y1 + (1r-z)*y2 in N by A1,A2,A8,A6;
    hence thesis by A9;
  end;
  hence thesis;
end;

theorem
  for V being ComplexLinearSpace, M,N being Subset of V st M is convex &
  N is convex holds M - N is convex
proof
  let V be ComplexLinearSpace;
  let M,N be Subset of V;
  assume
A1: M is convex & N is convex;
  for u,v being VECTOR of V, z being Complex st (ex r being Real st z=r &
  0 < r & r < 1) & u in M-N & v in M-N holds z*u + (1r-z)*v in M-N
  proof
    let u,v be VECTOR of V;
    let z be Complex;
    assume that
A2: ex r being Real st z=r & 0 < r & r < 1 and
A3: u in M-N and
A4: v in M-N;
    consider x2,y2 being Element of V such that
A5: v = x2 - y2 and
A6: x2 in M & y2 in N by A4;
    consider x1,y1 being Element of V such that
A7: u = x1 - y1 and
A8: x1 in M & y1 in N by A3;
A9: z*u + (1r-z)*v = z*x1 - z*y1 + (1r-z)*(x2-y2) by A7,A5,CLVECT_1:9
      .= z*x1 - z*y1 + ((1r-z)*x2 - (1r-z)*y2) by CLVECT_1:9
      .= z*x1 - z*y1 + (1r-z)*x2 - (1r-z)*y2 by RLVECT_1:def 3
      .= z*x1 - (z*y1 - (1r-z)*x2) - (1r-z)*y2 by RLVECT_1:29
      .= z*x1 + ((1r-z)*x2 + (-z*y1)) - (1r-z)*y2 by RLVECT_1:33
      .= z*x1 + (1r-z)*x2 + (-z*y1) - (1r-z)*y2 by RLVECT_1:def 3
      .= z*x1 + (1r-z)*x2 + ((-z*y1) - (1r-z)*y2) by RLVECT_1:def 3
      .= (z*x1 + (1r-z)*x2) - (z*y1 + (1r-z)*y2) by RLVECT_1:30;
    z*x1 + (1r-z)*x2 in M & z*y1 + (1r-z)*y2 in N by A1,A2,A8,A6;
    hence thesis by A9;
  end;
  hence thesis;
end;

theorem Th48:
  for V being non empty CLSStruct, M being Subset of V holds M is
  convex iff for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
  holds z*M + (1r-z)*M c= M
proof
  let V be non empty CLSStruct;
  let M be Subset of V;
A1: M is convex implies for z being Complex st (ex r being Real st z=r & 0 <
  r & r < 1) holds z*M + (1r-z)*M c= M
  proof
    assume
A2: M is convex;
    let z be Complex;
    assume
A3: ex r being Real st z=r & 0 < r & r < 1;
    for x being Element of V st x in z*M + (1r-z)*M holds x in M
    proof
      let x be Element of V;
      assume x in z*M + (1r-z)*M;
      then consider u,v be Element of V such that
A4:   x = u + v and
A5:   u in z*M & v in (1r-z)*M;
      ( ex w1 be Element of V st u = z * w1 & w1 in M)& ex w2 be Element
      of V st v = (1r-z)*w2 & w2 in M by A5;
      hence thesis by A2,A3,A4;
    end;
    hence thesis;
  end;
  ( for z being Complex st ( ex r being Real st z=r & 0 < r & r < 1 )
  holds z*M + (1r-z)*M c= M ) implies M is convex
  proof
    assume
A6: for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
    holds z*M + (1r-z)*M c= M;
    let u,v be VECTOR of V;
    let z be Complex;
    assume ex r being Real st z=r & 0 < r & r < 1;
    then
A7: z*M + (1r-z)*M c= M by A6;
    assume u in M & v in M;
    then z*u in z*M & (1r-z)*v in (1r-z)*M;
    then z*u + (1r-z)*v in z*M + (1r-z)*M;
    hence thesis by A7;
  end;
  hence thesis by A1;
end;

theorem
  for V being Abelian non empty CLSStruct, M being Subset of V st M is
  convex holds for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
  holds (1r-z)*M + z*M c= M
proof
  let V be Abelian non empty CLSStruct;
  let M be Subset of V;
  assume
A1: M is convex;
  let z be Complex;
  assume
A2: ex r being Real st z=r & 0 < r & r < 1;
  for x being Element of V st x in (1r-z)*M + z*M holds x in M
  proof
    let x be Element of V;
    assume x in (1r-z)*M + z*M;
    then consider u,v be Element of V such that
A3: x = u + v and
A4: u in (1r-z)*M & v in z*M;
    ( ex w1 be Element of V st u = (1r-z) * w1 & w1 in M)& ex w2 be
    Element of V st v = z*w2 & w2 in M by A4;
    hence thesis by A1,A2,A3;
  end;
  hence thesis;
end;

theorem
  for V being Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty
  CLSStruct, M,N being Subset of V st M is convex & N is convex holds for z
  being Complex holds z*M + (1r-z)*N is convex
proof
  let V be Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty
  CLSStruct;
  let M,N be Subset of V;
  assume that
A1: M is convex and
A2: N is convex;
  let z be Complex;
  let u,v be VECTOR of V;
  let s be Complex;
  assume that
A3: ex p being Real st s=p & 0 < p & p < 1 and
A4: u in z*M + (1r-z)*N and
A5: v in z*M + (1r-z)*N;
  consider x2,y2 be VECTOR of V such that
A6: v = x2 + y2 and
A7: x2 in z*M and
A8: y2 in (1r-z)*N by A5;
  consider x1,y1 be VECTOR of V such that
A9: u = x1 + y1 and
A10: x1 in z*M and
A11: y1 in (1r-z)*N by A4;
  consider mx2 be VECTOR of V such that
A12: x2 = z*mx2 and
A13: mx2 in M by A7;
  consider mx1 be VECTOR of V such that
A14: x1 = z*mx1 and
A15: mx1 in M by A10;
A16: s*x1 + (1r-s)*x2 = s*z*mx1 + (1r-s)*(z*mx2) by A14,A12,CLVECT_1:def 4
    .= s*z*mx1 + (1r-s)*z*mx2 by CLVECT_1:def 4
    .= z*(s*mx1) + (1r-s)*z*mx2 by CLVECT_1:def 4
    .= z*(s*mx1) + z*((1r-s)*mx2) by CLVECT_1:def 4
    .= z*(s*mx1 + (1r-s)*mx2) by CLVECT_1:def 2;
  consider ny2 be VECTOR of V such that
A17: y2 = (1r-z)*ny2 and
A18: ny2 in N by A8;
  consider ny1 be VECTOR of V such that
A19: y1 = (1r-z)*ny1 and
A20: ny1 in N by A11;
A21: s*y1 + (1r-s)*y2 = s*(1r-z)*ny1 + (1r-s)*((1r-z)*ny2) by A19,A17,
CLVECT_1:def 4
    .= s*(1r-z)*ny1 + (1r-s)*(1r-z)*ny2 by CLVECT_1:def 4
    .= (1r-z)*(s*ny1) + (1r-s)*(1r-z)*ny2 by CLVECT_1:def 4
    .= (1r-z)*(s*ny1) + (1r-z)*((1r-s)*ny2) by CLVECT_1:def 4
    .= (1r-z)*(s*ny1 + (1r-s)*ny2) by CLVECT_1:def 2;
  s*ny1 + (1r-s)*ny2 in N by A2,A3,A20,A18;
  then
A22: s*y1 + (1r-s)*y2 in (1r-z)*N by A21;
  s*mx1 + (1r-s)*mx2 in M by A1,A3,A15,A13;
  then
A23: s*x1 + (1r-s)*x2 in z*M by A16;
  s*u + (1r-s)*v = s*x1 + s*y1 + (1r-s)*(x2 + y2) by A9,A6,CLVECT_1:def 2
    .= s*x1 + s*y1 + ((1r-s)*x2 + (1r-s)*y2) by CLVECT_1:def 2
    .= s*x1 + s*y1 + (1r-s)*x2 + (1r-s)*y2 by RLVECT_1:def 3
    .= s*x1 + (1r-s)*x2 + s*y1 + (1r-s)*y2 by RLVECT_1:def 3
    .= (s*x1 + (1r-s)*x2) + (s*y1 + (1r-s)*y2) by RLVECT_1:def 3;
  hence thesis by A23,A22;
end;

theorem Th51:
  for V being vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct, M be
  Subset of V holds 1r*M = M
proof
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct;
  let M be Subset of V;
  for v being Element of V st v in M holds v in 1r*M
  proof
    let v be Element of V;
A1: v = 1r*v by CLVECT_1:def 5;
    assume v in M;
    hence thesis by A1;
  end;
  then
A2: M c= 1r*M;
  for v being Element of V st v in 1r*M holds v in M
  proof
    let v be Element of V;
    assume v in 1r*M;
    then ex x be Element of V st v = 1r*x & x in M;
    hence thesis by CLVECT_1:def 5;
  end;
  then 1r*M c= M;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem Th52:
  for V being ComplexLinearSpace, M be non empty Subset of V holds
  0c * M = {0.V}
proof
  let V be ComplexLinearSpace;
  let M be non empty Subset of V;
  for v being Element of V st v in {0.V} holds v in 0c * M
  proof
    let v be Element of V;
    consider x being object such that
A1: x in M by XBOOLE_0:def 1;
    reconsider x as Element of V by A1;
    assume v in {0.V};
    then v = 0.V by TARSKI:def 1;
    then v = 0c * x by CLVECT_1:1;
    hence thesis by A1;
  end;
  then
A2: {0.V} c= 0c * M;
  for v being Element of V st v in 0c * M holds v in {0.V}
  proof
    let v be Element of V;
    assume v in 0c * M;
    then ex x be Element of V st v = 0c * x & x in M;
    then v = 0.V by CLVECT_1:1;
    hence thesis by TARSKI:def 1;
  end;
  then 0c * M c= {0.V};
  hence thesis by A2,XBOOLE_0:def 10;
end;

::$CT

theorem Th53:
  for V being vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct, M
  being Subset of V, z1,z2 being Complex holds z1*(z2*M) = (z1*z2)*M
proof
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct;
  let M be Subset of V;
  let z1,z2 be Complex;
  for x being VECTOR of V st x in z1*(z2*M) holds x in (z1*z2)*M
  proof
    let x be VECTOR of V;
    assume x in z1*(z2*M);
    then consider w1 be VECTOR of V such that
A1: x = z1*w1 and
A2: w1 in z2*M;
    consider w2 be VECTOR of V such that
A3: w1 = z2*w2 and
A4: w2 in M by A2;
    x = (z1*z2)*w2 by A1,A3,CLVECT_1:def 4;
    hence thesis by A4;
  end;
  then
A5: z1*(z2*M) c= (z1*z2)*M;
  for x being VECTOR of V st x in (z1*z2)*M holds x in z1*(z2*M)
  proof
    let x be VECTOR of V;
    assume x in (z1*z2)*M;
    then consider w1 be VECTOR of V such that
A6: x = (z1*z2)*w1 & w1 in M;
    x = z1*(z2*w1) & z2*w1 in z2*M by A6,CLVECT_1:def 4;
    hence thesis;
  end;
  then (z1*z2)*M c= z1*(z2*M);
  hence thesis by A5,XBOOLE_0:def 10;
end;

theorem Th54:
  for V being vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct, M1,M2
  being Subset of V, z being Complex holds z*(M1 + M2) = z*M1 + z*M2
proof
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct;
  let M1,M2 be Subset of V;
  let z be Complex;
  for x being VECTOR of V st x in z*M1 + z*M2 holds x in z*(M1+M2)
  proof
    let x be VECTOR of V;
    assume x in z*M1 + z*M2;
    then consider w1,w2 be VECTOR of V such that
A1: x = w1 + w2 and
A2: w1 in z*M1 and
A3: w2 in z*M2;
    consider v2 be VECTOR of V such that
A4: w2 = z * v2 and
A5: v2 in M2 by A3;
    consider v1 be VECTOR of V such that
A6: w1 = z * v1 and
A7: v1 in M1 by A2;
A8: v1 + v2 in M1 + M2 by A7,A5;
    x = z*(v1 + v2) by A1,A6,A4,CLVECT_1:def 2;
    hence thesis by A8;
  end;
  then
A9: z*M1 + z*M2 c= z*(M1+M2);
  for x being VECTOR of V st x in z*(M1+M2) holds x in z*M1 + z*M2
  proof
    let x be VECTOR of V;
    assume x in z*(M1+M2);
    then consider w9 be VECTOR of V such that
A10: x = z*w9 and
A11: w9 in M1 + M2;
    consider w1,w2 be VECTOR of V such that
A12: w9 = w1 + w2 and
A13: w1 in M1 & w2 in M2 by A11;
A14: z*w1 in z*M1 & z*w2 in z*M2 by A13;
    x = z*w1 + z*w2 by A10,A12,CLVECT_1:def 2;
    hence thesis by A14;
  end;
  then z*(M1 + M2) c= z*M1 + z*M2;
  hence thesis by A9,XBOOLE_0:def 10;
end;

theorem
  for V being ComplexLinearSpace, M being Subset of V, v being VECTOR of
  V holds M is convex iff v + M is convex
proof
  let V be ComplexLinearSpace;
  let M be Subset of V;
  let v be VECTOR of V;
A1: v + M is convex implies M is convex
  proof
    assume
A2: v + M is convex;
    let w1,w2 be VECTOR of V;
    let z be Complex;
    assume that
A3: ex r being Real st z=r & 0 < r & r < 1 and
A4: w1 in M & w2 in M;
    set x1 = v + w1, x2 = v + w2;
    x1 in v + M & x2 in {v + w where w is VECTOR of V : w in M} by A4;
    then
A5: z*x1 + (1r-z)*x2 in v + M by A2,A3;
    z*x1 + (1r-z)*x2 = z*v + z*w1 + (1r-z)*(v + w2) by CLVECT_1:def 2
      .= z*v + z*w1 + ((1r-z)*v + (1r-z)*w2) by CLVECT_1:def 2
      .= z*v + z*w1 + (1r-z)*v + (1r-z)*w2 by RLVECT_1:def 3
      .= z*v + (1r-z)*v + z*w1 + (1r-z)*w2 by RLVECT_1:def 3
      .= (z+(1r-z))*v + z*w1 + (1r-z)*w2 by CLVECT_1:def 3
      .= v + z*w1 + (1r-z)*w2 by CLVECT_1:def 5
      .= v + (z*w1 + (1r-z)*w2) by RLVECT_1:def 3;
    then
    ex w be VECTOR of V st v + (z*w1 + (1r-z)*w2) = v + w & w in M by A5;
    hence thesis by RLVECT_1:8;
  end;
  M is convex implies v + M is convex
  proof
    assume
A6: M is convex;
    let w1,w2 be VECTOR of V;
    let z be Complex;
    assume that
A7: ex r being Real st z=r & 0 < r & r < 1 and
A8: w1 in v + M and
A9: w2 in v + M;
    consider x2 be VECTOR of V such that
A10: w2 = v + x2 and
A11: x2 in M by A9;
    consider x1 be VECTOR of V such that
A12: w1 = v + x1 and
A13: x1 in M by A8;
A14: z*w1 + (1r-z)*w2 = z*v + z*x1 + (1r-z)*(v+x2) by A12,A10,CLVECT_1:def 2
      .= z*v + z*x1 + ((1r-z)*v + (1r-z)*x2) by CLVECT_1:def 2
      .= z*v + z*x1 + (1r-z)*v + (1r-z)*x2 by RLVECT_1:def 3
      .= z*v + (1r-z)*v + z*x1 + (1r-z)*x2 by RLVECT_1:def 3
      .= (z+(1r-z))*v + z*x1 + (1r-z)*x2 by CLVECT_1:def 3
      .= v + z*x1 + (1r-z)*x2 by CLVECT_1:def 5
      .= v + (z*x1 + (1r-z)*x2) by RLVECT_1:def 3;
    z*x1 + (1r-z)*x2 in M by A6,A7,A13,A11;
    hence thesis by A14;
  end;
  hence thesis by A1;
end;

theorem
  for V being ComplexLinearSpace holds Up((0).V) is convex
proof
  let V be ComplexLinearSpace;
  let u,v be VECTOR of V;
  let z be Complex;
  assume that
  ex r being Real st z=r & 0 < r & r < 1 and
A1: u in Up((0).V) and
A2: v in Up((0).V);
  v in {0.V} by A2,CLVECT_1:def 9;
  then
A3: v = 0.V by TARSKI:def 1;
  u in {0.V} by A1,CLVECT_1:def 9;
  then u = 0.V by TARSKI:def 1;
  then z * u + (1r-z) * v = 0.V + (1r-z) * 0.V by A3,CLVECT_1:1
    .= 0.V + 0.V by CLVECT_1:1
    .= 0.V;
  then z * u + (1r-z) * v in {0.V} by TARSKI:def 1;
  hence thesis by CLVECT_1:def 9;
end;

theorem
  for V being ComplexLinearSpace holds Up((Omega).V) is convex;

theorem
  for V being non empty CLSStruct, M being Subset of V st M = {}
  holds M is convex;

theorem Th59:
  for V being Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non
empty CLSStruct, M1,M2 being Subset of V, z1,z2 being Complex st M1 is convex
  & M2 is convex holds z1*M1 + z2*M2 is convex
proof
  let V be Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty
  CLSStruct;
  let M1,M2 be Subset of V;
  let z1,z2 be Complex;
  assume that
A1: M1 is convex and
A2: M2 is convex;
  let u,v be VECTOR of V;
  let s be Complex;
  assume that
A3: ex p being Real st s=p & 0 < p & p < 1 and
A4: u in z1*M1 + z2*M2 and
A5: v in z1*M1 + z2*M2;
  consider v1,v2 be VECTOR of V such that
A6: v = v1 + v2 and
A7: v1 in z1*M1 and
A8: v2 in z2*M2 by A5;
  consider u1,u2 be VECTOR of V such that
A9: u = u1 + u2 and
A10: u1 in z1*M1 and
A11: u2 in z2*M2 by A4;
  consider y1 be VECTOR of V such that
A12: v1 = z1*y1 and
A13: y1 in M1 by A7;
  consider x1 be VECTOR of V such that
A14: u1 = z1*x1 and
A15: x1 in M1 by A10;
A16: s*u1 + (1r-s)*v1 = z1*s*x1 + (1r-s)*(z1*y1) by A14,A12,CLVECT_1:def 4
    .= z1*s*x1 + z1*(1r-s)*y1 by CLVECT_1:def 4
    .= z1*(s*x1) + z1*(1r-s)*y1 by CLVECT_1:def 4
    .= z1*(s*x1) + z1*((1r-s)*y1) by CLVECT_1:def 4
    .= z1*(s*x1 + (1r-s)*y1) by CLVECT_1:def 2;
  consider y2 be VECTOR of V such that
A17: v2 = z2*y2 and
A18: y2 in M2 by A8;
  consider x2 be VECTOR of V such that
A19: u2 = z2*x2 and
A20: x2 in M2 by A11;
A21: s*u2 + (1r-s)*v2 = z2*s*x2 + (1r-s)*(z2*y2) by A19,A17,CLVECT_1:def 4
    .= z2*s*x2 + z2*(1r-s)*y2 by CLVECT_1:def 4
    .= z2*(s*x2) + z2*(1r-s)*y2 by CLVECT_1:def 4
    .= z2*(s*x2) + z2*((1r-s)*y2) by CLVECT_1:def 4
    .= z2*(s*x2 + (1r-s)*y2) by CLVECT_1:def 2;
  s*x2 + (1r-s)*y2 in M2 by A2,A3,A20,A18;
  then
A22: s*u2 + (1r-s)*v2 in z2*M2 by A21;
  s*x1 + (1r-s)*y1 in M1 by A1,A3,A15,A13;
  then
A23: s*u1 + (1r-s)*v1 in z1*M1 by A16;
  s*(u1+u2) + (1r-s)*(v1+v2) = s*u1 + s*u2 + (1r-s)*(v1+v2) by CLVECT_1:def 2
    .= s*u1 + s*u2 + ((1r-s)*v1 + (1r-s)*v2) by CLVECT_1:def 2
    .= s*u1 + s*u2 + (1r-s)*v1 + (1r-s)*v2 by RLVECT_1:def 3
    .= s*u1 + (1r-s)*v1 + s*u2 + (1r-s)*v2 by RLVECT_1:def 3
    .= s*u1 + (1r-s)*v1 + (s*u2 + (1r-s)*v2) by RLVECT_1:def 3;
  hence thesis by A9,A6,A23,A22;
end;

theorem Th60:
  for V being vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct, M
  being Subset of V, z1,z2 being Complex holds (z1 + z2)*M c= z1*M + z2*M
proof
  let V be vector-distributive scalar-distributive scalar-associative
  scalar-unital non empty CLSStruct;
  let M be Subset of V;
  let z1,z2 be Complex;
  for x being VECTOR of V st x in (z1+z2)*M holds x in z1*M + z2*M
  proof
    let x be VECTOR of V;
    assume x in (z1+z2)*M;
    then consider w be VECTOR of V such that
A1: x = (z1 + z2)*w and
A2: w in M;
A3: z2*w in z2*M by A2;
    x = z1*w + z2*w & z1*w in z1*M by A1,A2,CLVECT_1:def 3;
    hence thesis by A3;
  end;
  hence thesis;
end;

theorem Th61:
  for V being non empty CLSStruct, M,N being Subset of V, z being
  Complex st M c= N holds z*M c= z*N
proof
  let V be non empty CLSStruct;
  let M,N be Subset of V;
  let z be Complex;
  assume
A1: M c= N;
  now
    let x be VECTOR of V;
    assume x in z*M;
    then ex w be VECTOR of V st x = z*w & w in M;
    hence x in z*N by A1;
  end;
  hence thesis;
end;

theorem Th62:
  for V being non empty CLSStruct, M being empty Subset of V, z
  being Complex holds z * M = {}
proof
  let V be non empty CLSStruct;
  let M be empty Subset of V;
  let z be Complex;
  now
    let x be VECTOR of V;
    assume x in z * M;
    then ex v be VECTOR of V st x = z * v & v in {};
    hence x in {};
  end;
  then z * M c= {};
  hence thesis;
end;

Lm2: for V being ComplexLinearSpace, M being Subset of V, z1,z2 being Complex
st (ex r1,r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0 ) & M is convex
holds z1*M + z2*M c= (z1 + z2)*M
proof
  let V be ComplexLinearSpace;
  let M be Subset of V;
  let z1,z2 be Complex;
  assume that
A1: ex r1, r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0 and
A2: M is convex;
  consider r1, r2 being Real such that
A3: z1=r1 and
A4: z2=r2 and
A5: r1 >= 0 and
A6: r2 >= 0 by A1;
  per cases;
  suppose
    M is empty;
    then z1*M = {} & (z1+z2)*M = {} by Th62;
    hence thesis by CONVEX1:40;
  end;
  suppose
A7: M is non empty;
    per cases;
    suppose
A8:   z1 = 0;
      then z1*M = {0.V} by A7,Th52;
      hence thesis by A8,CONVEX1:35;
    end;
    suppose
A9:   z2 = 0;
      then z2*M = {0.V} by A7,Th52;
      hence thesis by A9,CONVEX1:35;
    end;
    suppose
A10:  z1 <> 0 & z2 <> 0;
      then r1 + r2 > r1 by A4,A6,XREAL_1:29;
      then r1/(r1+r2) < 1 by A5,XREAL_1:189;
      then
      z1/(z1+z2) * M + (1r - z1/(z1+z2)) * M c= M by A2,A3,A4,A5,A6,A10,Th48;
      then
A11:  (z1+z2)*(z1/(z1+z2)*M + (1r-z1/(z1+z2))*M) c= (z1+z2)*M by Th61;
      1-r1/(r1+r2) = (r1+r2)/(r1+r2) - r1/(r1+r2) by A3,A5,A6,A10,XCMPLX_1:60;
      then 1-r1/(r1+r2) = (r1+r2-r1)/(r1+r2);
      then
A12:  (z1+z2)*((1r-z1/(z1+z2))*M) = z2/(z1+z2)*(z1+z2)*M by A3,A4,Th53
        .= z2*M by A3,A4,A5,A6,A10,XCMPLX_1:87;
      (z1+z2)*(z1/(z1+z2)*M) = (z1/(z1+z2))*(z1+z2)*M by Th53
        .= z1*M by A3,A4,A5,A6,A10,XCMPLX_1:87;
      hence thesis by A11,A12,Th54;
    end;
  end;
end;

::$CT 2

theorem
  for V being ComplexLinearSpace, M being Subset of V, z1,z2 being
  Complex st (ex r1,r2 being Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0) & M
  is convex holds z1*M + z2*M = (z1 + z2)*M
proof
  let V be ComplexLinearSpace, M be Subset of V, z1,z2 be Complex;
  assume
  ( ex r1,r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0)& M is convex;
  hence z1*M + z2*M c= (z1 + z2)*M by Lm2;
  thus thesis by Th60;
end;

theorem
  for V being Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty
CLSStruct, M1,M2,M3 being Subset of V, z1,z2,z3 being Complex st M1 is convex
  & M2 is convex & M3 is convex holds z1*M1 + z2*M2 + z3*M3 is convex
proof
  let V be Abelian add-associative vector-distributive scalar-distributive
  scalar-associative scalar-unital non empty
  CLSStruct;
  let M1,M2,M3 be Subset of V;
  let z1,z2,z3 be Complex;
  assume that
A1: M1 is convex & M2 is convex and
A2: M3 is convex;
  z1*M1 + z2*M2 is convex by A1,Th59;
  then 1r*(z1*M1 + z2*M2) + z3*M3 is convex by A2,Th59;
  hence thesis by Th51;
end;

theorem Th65:
  for V being non empty CLSStruct, F being Subset-Family of V st (
  for M being Subset of V st M in F holds M is convex) holds meet F is convex
proof
  let V be non empty CLSStruct;
  let F be Subset-Family of V;
  assume
A1: for M being Subset of V st M in F holds M is convex;
  per cases;
  suppose
    F = {};
    then meet F = {} by SETFAM_1:def 1;
    hence thesis;
  end;
  suppose
A2: F <> {};
    thus meet F is convex
    proof
      let u,v be VECTOR of V;
      let z be Complex;
      assume that
A3:   ex r being Real st z=r & 0 < r & r < 1 and
A4:   u in meet F and
A5:   v in meet F;
      for M being set st M in F holds z*u + (1r-z)*v in M
      proof
        let M be set;
        assume
A6:     M in F;
        then reconsider M as Subset of V;
A7:     v in M by A5,A6,SETFAM_1:def 1;
        M is convex & u in M by A1,A4,A6,SETFAM_1:def 1;
        hence thesis by A3,A7;
      end;
      hence thesis by A2,SETFAM_1:def 1;
    end;
  end;
end;

theorem Th66:
  for V being non empty CLSStruct, M being Subset of V st M is
  Affine holds M is convex
proof
  let V be non empty CLSStruct;
  let M be Subset of V;
  assume
A1: M is Affine;
  let u,v be VECTOR of V;
  let z be Complex;
  assume that
A2: ex r being Real st z=r & 0 < r & r < 1 and
A3: u in M & v in M;
  set s = 1r-z;
  consider r being Real such that
A4: z=r and
  0 < r and
  r < 1 by A2;
  s=1-r by A4;
  then (1r-s)*u+s*v in M by A1,A3;
  hence thesis;
end;

registration
  let V be non empty CLSStruct;
  cluster non empty convex for Subset of V;
  existence
  proof
    set M = the non empty Affine Subset of V;
    M is convex by Th66;
    hence thesis;
  end;
end;

registration
  let V be non empty CLSStruct;
  cluster empty convex for Subset of V;
  existence
  proof
    {}V is convex;
    hence thesis;
  end;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Re(u .|. v) >= r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) >= r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) >= r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Re(y.|.v) >= (1-p)*r by A5,XREAL_1:64;
  ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) >= r by A1,A3;
  then p*Re(x.|.v) >= p*r by A7,XREAL_1:64;
  then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) >= p*r + (1-p)*r by A9,XREAL_1:7;
  Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
    .= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Re(u .|. v) > r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) > r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) > r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Re(y.|.v) > (1-p)*r by A5,XREAL_1:68;
  ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) > r by A1,A3;
  then p*Re(x.|.v) > p*r by A7,XREAL_1:68;
  then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) > p*r + (1-p)*r by A9,XREAL_1:8;
  Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
    .= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Re(u .|. v) <= r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) <= r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) <= r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Re(y.|.v) <= (1-p)*r by A5,XREAL_1:64;
  ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) <= r by A1,A3;
  then p*Re(x.|.v) <= p*r by A7,XREAL_1:64;
  then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) <= p*r + (1-p)*r by A9,XREAL_1:7;
  Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
    .= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Re(u .|. v) < r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) < r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) < r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Re(y.|.v) < (1-p)*r by A5,XREAL_1:68;
  ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) < r by A1,A3;
  then p*Re(x.|.v) < p*r by A7,XREAL_1:68;
  then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) < p*r + (1-p)*r by A9,XREAL_1:8;
  Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
    .= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Im(u .|. v) >= r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) >= r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) >= r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Im(y.|.v) >= (1-p)*r by A5,XREAL_1:64;
  ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) >= r by A1,A3;
  then p*Im(x.|.v) >= p*r by A7,XREAL_1:64;
  then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) >= p*r + (1-p)*r by A9,XREAL_1:7;
  Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
    .= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Im(u .|. v) > r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) > r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) > r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Im(y.|.v) > (1-p)*r by A5,XREAL_1:68;
  ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) > r by A1,A3;
  then p*Im(x.|.v) > p*r by A7,XREAL_1:68;
  then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) > p*r + (1-p)*r by A9,XREAL_1:8;
  Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
    .= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Im(u .|. v) <= r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) <= r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) <= r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Im(y.|.v) <= (1-p)*r by A5,XREAL_1:64;
  ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) <= r by A1,A3;
  then p*Im(x.|.v) <= p*r by A7,XREAL_1:64;
  then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) <= p*r + (1-p)*r by A9,XREAL_1:7;
  Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
    .= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : Im(u .|. v) < r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) < r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) < r by A1,A4;
  consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
  1-p > 0 by A8,XREAL_1:50;
  then
A9: (1-p)*Im(y.|.v) < (1-p)*r by A5,XREAL_1:68;
  ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) < r by A1,A3;
  then p*Im(x.|.v) < p*r by A7,XREAL_1:68;
  then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) < p*r + (1-p)*r by A9,XREAL_1:8;
  Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
    .= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
    .= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
    .= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
    .= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
  hence thesis by A1,A10;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : |.u .|. v .| <= r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : |.u.|.v.| <= r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
  consider p being Real such that
A5: s=p and
A6: 0 < p and
A7: p < 1 by A2;
A8: 1-p > 0 by A7,XREAL_1:50;
  ex u2 be VECTOR of V st y = u2 & |.u2.|.v.| <= r by A1,A4;
  then
A9: (1-p)*|.y.|.v.| <= (1-p)*r by A8,XREAL_1:64;
  ex u1 be VECTOR of V st x = u1 & |.u1.|.v.| <= r by A1,A3;
  then p*|.x.|.v.| <= p*r by A6,XREAL_1:64;
  then
A10: p*|.x.|.v.|+(1-p)*|.y.|.v.| <= p*r + (1-p)*r by A9,XREAL_1:7;
  |.s*(x.|.v).| = p*|.x.|.v.| & |.(1r-s)*(y.|.v).| = (1-p)*|.y.|.v.| by A5,A6
,A7,Th44;
  then
A11: |.s*(x.|.v)+(1r-s)*(y.|.v).| <= p*|.x.|.v.| + (1-p)*|.y.|.v.| by
COMPLEX1:56;
  |.(s*x+(1r-s)*y).|.v.| = |.(s*x).|.v+((1r-s)*y).|.v.| by CSSPACE:def 13
    .= |.s*(x.|.v)+((1r-s)*y).|.v.| by CSSPACE:def 13
    .= |. s*(x.|.v)+(1r-s)*(y.|.v).| by CSSPACE:def 13;
  then |.(s*x+(1r-s)*y).|.v.| <= r by A11,A10,XXREAL_0:2;
  hence thesis by A1;
end;

theorem
  for V being ComplexUnitarySpace-like non empty CUNITSTR, M being
Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V
  : |.u .|. v .| < r } holds M is convex
proof
  let V be ComplexUnitarySpace-like non empty CUNITSTR;
  let M be Subset of V;
  let v be VECTOR of V;
  let r be Real;
  assume
A1: M = {u where u is VECTOR of V : |.u.|.v.| < r };
  let x,y be VECTOR of V;
  let s be Complex;
  assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
  consider p being Real such that
A5: s=p and
A6: 0 < p and
A7: p < 1 by A2;
A8: 1-p > 0 by A7,XREAL_1:50;
  ex u2 be VECTOR of V st y = u2 & |.u2.|.v.| < r by A1,A4;
  then
A9: (1-p)*|.y.|.v.| < (1-p)*r by A8,XREAL_1:68;
  ex u1 be VECTOR of V st x = u1 & |.u1.|.v.| < r by A1,A3;
  then p*|.x.|.v.| < p*r by A6,XREAL_1:68;
  then
A10: p*|.x.|.v.|+(1-p)*|.y.|.v.| < p*r + (1-p)*r by A9,XREAL_1:8;
  |.s*(x.|.v).| = p*|.x.|.v.| & |.(1r-s)*(y.|.v).| = (1-p)*|.y.|.v.| by A5,A6
,A7,Th44;
  then
A11: |.s*(x.|.v)+(1r-s)*(y.|.v).| <= p*|.x.|.v.| + (1-p)*|.y.|.v.| by
COMPLEX1:56;
  |.(s*x+(1r-s)*y).|.v.| = |.(s*x).|.v+((1r-s)*y).|.v.| by CSSPACE:def 13
    .= |.s*(x.|.v)+((1r-s)*y).|.v.| by CSSPACE:def 13
    .= |. s*(x.|.v)+(1r-s)*(y.|.v).| by CSSPACE:def 13;
  then |.(s*x+(1r-s)*y).|.v.| < r by A11,A10,XXREAL_0:2;
  hence thesis by A1;
end;

begin  :: Complex Convex Combinations

definition
  let V be ComplexLinearSpace, L be C_Linear_Combination of V;
  attr L is convex means

  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;

theorem Th77:
  for V being ComplexLinearSpace, L being C_Linear_Combination of
  V st L is convex holds Carrier L <> {}
proof
  let V be ComplexLinearSpace;
  let L be C_Linear_Combination of V;
  assume L is convex;
  then consider F being FinSequence of the carrier of V such that
A1: F is one-to-one & rng F = Carrier L and
A2: 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;
 consider f being FinSequence of REAL such that
A3:  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 A2;
  assume Carrier L = {};
  then len F = 0 by A1,CARD_1:27,FINSEQ_4:62;
  then f = <*>the carrier of V by A3;
  hence contradiction by A3,RVSUM_1:72;
end;

theorem
  for V being ComplexLinearSpace, L being C_Linear_Combination of V, v
  being VECTOR of V st L is convex & ( ex r being Real st r = L.v & r <= 0 )
  holds not v in Carrier L
proof
  let V be ComplexLinearSpace;
  let L be C_Linear_Combination of V;
  let v be VECTOR of V;
  assume that
A1: L is convex and
A2: ex r being Real st r = L.v & r <= 0;
  consider r being Real such that
A3: r = L.v and
A4: r <= 0 by A2;
  per cases by A4;
  suppose
    r = 0;
    hence thesis by A3,Th1;
  end;
  suppose
A5: r < 0;
    now
      consider F being FinSequence of the carrier of V such that
      F is one-to-one and
A6:   rng F = Carrier L and
A7:   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;
      assume v in Carrier L;
      then consider n be object such that
A8:   n in dom F and
A9:   F.n = v by A6,FUNCT_1:def 3;
      reconsider n as Element of NAT by A8;
      consider f being FinSequence of REAL such that
A10:  len f = len F and
      Sum f = 1 and
A11:  for n being Nat st n in dom f holds f.n =L.(F.n) & f.n >= 0 by A7;
      n in Seg len F by A8,FINSEQ_1:def 3;
      then
A12:  n in dom f by A10,FINSEQ_1:def 3;
      then L.v = f.n by A11,A9;
      hence contradiction by A3,A5,A11,A12;
    end;
    hence thesis;
  end;
end;

theorem
  for V being ComplexLinearSpace, L being C_Linear_Combination of V st L
  is convex holds L <> ZeroCLC V
proof
  let V be ComplexLinearSpace;
  let L be C_Linear_Combination of V;
  assume L is convex;
  then
A1: Carrier L <> {} by Th77;
  assume L = ZeroCLC V;
  hence contradiction by A1;
end;

theorem Th80:
  for V being ComplexLinearSpace, v being VECTOR of V, L being
  C_Linear_Combination of V st L is convex & Carrier L = {v} holds ( ex r being
  Real st r = L.v & r = 1 ) & Sum L = L.v * v
proof
  let V be ComplexLinearSpace;
  let v be VECTOR of V;
  let L be C_Linear_Combination of V;
  assume that
A1: L is convex and
A2: Carrier L = {v};
  reconsider L as C_Linear_Combination of {v} by A2,Def4;
  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;
A5: F = <*v*> by A2,A3,FINSEQ_3:97;
  consider f be 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;
  then
A11: f.1 = f/.1 by PARTFUN1:def 6;
  then
A12: f = <* r *> by A9,FINSEQ_1:def 8;
  f.1 = L.(F.1) by A8,A10;
  then r = L.v by A11,A5,FINSEQ_1:def 8;
  hence thesis by A7,A12,Th14,FINSOP_1:11;
end;

theorem Th81:
  for V being ComplexLinearSpace, v1,v2 being VECTOR of V, L being
C_Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds
( ex r1, r2 being Real st r1 = L.v1 & r2 = L.v2 & r1 + r2 = 1 & r1 >= 0 & r2 >=
  0 ) & Sum L = L.v1 * v1 + L.v2 * v2
proof
  let V be ComplexLinearSpace;
  let v1,v2 be VECTOR of V;
  let L be C_Linear_Combination of V;
  assume that
A1: L is convex and
A2: Carrier L = {v1,v2} and
A3: v1 <> v2;
  reconsider L as C_Linear_Combination of {v1,v2} by A2,Def4;
  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;
  consider f be 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,def 3;
  then
A11: 2 in dom f by TARSKI:def 2;
  then
A12: f.2 = L.(F.2) by A8;
  then f/.2 = L.(F.2) by A11,PARTFUN1:def 6;
  then reconsider r2 = L.(F.2) as Real;
A13: f.2 >= 0 by A8,A11;
A14: 1 in dom f by A10,TARSKI:def 2;
  then
A15: f.1 = L.(F.1) by A8;
  then f/.1 = L.(F.1) by A14,PARTFUN1:def 6;
  then reconsider r1 = L.(F.1) as Real;
A16: f = <*r1,r2*> by A9,A15,A12,FINSEQ_1:44;
  ex c1,c2 being Real st c1=L.v1 & c2=L.v2 & c1+c2=1 & c1>=0 &c2>=0
  proof
    per cases by A2,A3,A4,FINSEQ_3:99;
    suppose
      F = <*v1,v2*>;
      then
A17:  r1 = L.v1 & r2 = L.v2 by FINSEQ_1:44;
      r1 + r2 = 1 & r1 >= 0 by A7,A8,A14,A15,A16,RVSUM_1:77;
      hence thesis by A12,A13,A17;
    end;
    suppose
      F = <*v2,v1*>;
      then
A18:  r1 = L.v2 & r2 = L.v1 by FINSEQ_1:44;
      r1 + r2 = 1 & r1 >= 0 by A7,A8,A14,A15,A16,RVSUM_1:77;
      hence thesis by A12,A13,A18;
    end;
  end;
  hence thesis by A3,Th15;
end;

Lm3: for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V, L being
C_Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds
Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
  let V be ComplexLinearSpace;
  let v1,v2,v3 be VECTOR of V;
  let L be C_Linear_Combination of {v1,v2,v3};
  assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1;
A4: Carrier L c= {v1,v2,v3} by Def4;
  per cases by A4,ZFMISC_1:118;
  suppose
    Carrier L = {};
    then
A5: L = ZeroCLC V by Def3;
    then Sum L = 0.V by Th11
      .= 0.V + 0.V
      .= 0.V + 0.V + 0.V
      .= 0c * v1 + 0.V + 0.V by CLVECT_1:1
      .= 0c * v1 + 0c * v2 + 0.V by CLVECT_1:1
      .= 0c * v1 + 0c * v2 + 0c * v3 by CLVECT_1:1
      .= L.v1 * v1 + 0c * v2 + 0c * v3 by A5,Th2
      .= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A5,Th2
      .= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A5,Th2;
    hence thesis;
  end;
  suppose
A6: Carrier L = {v1};
    then reconsider L as C_Linear_Combination of {v1} by Def4;
A7: not v2 in Carrier L by A1,A6,TARSKI:def 1;
A8: not v3 in Carrier L by A3,A6,TARSKI:def 1;
    Sum L = L.v1 * v1 by Th14
      .= L.v1 * v1 + 0.V
      .= L.v1 * v1 + 0.V + 0.V
      .= L.v1 * v1 + 0c * v2 + 0.V by CLVECT_1:1
      .= L.v1 * v1 + 0c * v2 + 0c * v3 by CLVECT_1:1
      .= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A7
      .= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A8;
    hence thesis;
  end;
  suppose
A9: Carrier L = {v2};
    then reconsider L as C_Linear_Combination of {v2} by Def4;
A10: not v1 in Carrier L by A1,A9,TARSKI:def 1;
A11: not v3 in Carrier L by A2,A9,TARSKI:def 1;
    Sum L = L.v2 * v2 by Th14
      .= 0.V + L.v2 * v2
      .= 0.V + L.v2 * v2 + 0.V
      .= 0c * v1 + L.v2 * v2 + 0.V by CLVECT_1:1
      .= 0c * v1 + L.v2 * v2 + 0c * v3 by CLVECT_1:1
      .= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A10
      .= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A11;
    hence thesis;
  end;
  suppose
A12: Carrier L = {v3};
    then reconsider L as C_Linear_Combination of {v3} by Def4;
A13: not v1 in Carrier L by A3,A12,TARSKI:def 1;
A14: not v2 in Carrier L by A2,A12,TARSKI:def 1;
    Sum L = L.v3 * v3 by Th14
      .= 0.V + L.v3 * v3
      .= 0.V + 0.V + L.v3 * v3
      .= 0c * v1 + 0.V + L.v3 * v3 by CLVECT_1:1
      .= 0c * v1 + 0c * v2 + L.v3 * v3 by CLVECT_1:1
      .= L.v1 * v1 + 0c * v2 + L.v3 * v3 by A13
      .= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A14;
    hence thesis;
  end;
  suppose
A15: Carrier L = {v1,v2};
    then
A16: Sum L = L.v1 * v1 + L.v2 * v2 by A1,Th18
      .= L.v1 * v1 + L.v2 * v2 + 0.V
      .= L.v1 * v1 + L.v2 * v2 + 0c * v3 by CLVECT_1:1;
    not v3 in Carrier L by A2,A3,A15,TARSKI:def 2;
    hence thesis by A16;
  end;
  suppose
A17: Carrier L = {v1,v3};
    then
A18: Sum L = L.v1 * v1 + L.v3 * v3 by A3,Th18
      .= L.v1 * v1 + 0.V + L.v3 * v3
      .= L.v1 * v1 + 0c * v2 + L.v3 * v3 by CLVECT_1:1;
    not v2 in Carrier L by A1,A2,A17,TARSKI:def 2;
    hence thesis by A18;
  end;
  suppose
A19: Carrier L = {v2,v3};
    then
A20: Sum L = L.v2 * v2 + L.v3 * v3 by A2,Th18
      .= 0.V + L.v2 * v2 + L.v3 * v3
      .= 0c * v1 + L.v2 * v2 + L.v3 * v3 by CLVECT_1:1;
    not v1 in Carrier L by A1,A3,A19,TARSKI:def 2;
    hence thesis by A20;
  end;
  suppose
    Carrier L = {v1,v2,v3};
    then consider F be FinSequence of the carrier of V such that
A21: F is one-to-one & rng F = {v1,v2,v3} and
A22: Sum L = Sum(L (#) F) by Def6;
    F = <* v1,v2,v3 *> or F = <* v1,v3,v2 *> or F = <* v2,v1,v3 *> or F =
    <* v2,v3,v1 *> or F = <* v3,v1,v2 *> or F = <* v3,v2,v1 *> by A1,A2,A3,A21,
CONVEX1:31;
    then L (#) F = <* L.v1 * v1, L.v2 * v2, L.v3 * v3 *> or L (#) F = <* L.v1
* v1, L.v3 * v3, L.v2 * v2 *> or L (#) F = <* L.v2 * v2, L.v1 * v1, L.v3 * v3
*> or L (#) F = <* L.v2 * v2, L.v3 * v3, L.v1 * v1 *> or L (#) F = <* L.v3 * v3
, L.v1 * v1, L.v2 * v2 *> or L (#) F = <* L.v3 * v3, L.v2 * v2, L.v1 * v1 *>
by Th10;
    then Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3 or Sum L = L.v1 * v1 + (L.
    v2 * v2 + L.v3 * v3) or Sum L = L.v2 * v2 + (L.v1 * v1 + L.v3 * v3) by A22,
RLVECT_1:46;
    hence thesis by RLVECT_1:def 3;
  end;
end;

theorem Th82:
  for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V, L
being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <>
v2 & v2 <> v3 & v3 <> v1 holds ( ex r1, r2, r3 being Real st r1 = L.v1 &
r2 = L.v2 & r3 = L.v3 & r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum
  L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
  let V be ComplexLinearSpace;
  let v1,v2,v3 be VECTOR of V;
  let L be C_Linear_Combination of V;
  assume that
A1: L is convex and
A2: Carrier L = {v1,v2,v3} and
A3: v1 <> v2 & v2 <> v3 & v3 <> v1;
  reconsider L as C_Linear_Combination of {v1,v2,v3} by A2,Def4;
  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;
  consider f be 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,v3} by A2,A4,FINSEQ_4:62;
  then
A9: len f = 3 by A3,A6,CARD_2:58;
  then
A10: dom f = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
  then
A11: 2 in dom f by ENUMSET1:def 1;
  then
A12: f.2 = L.(F.2) by A8;
  then f/.2 = L.(F.2) by A11,PARTFUN1:def 6;
  then reconsider r2 = L.(F.2) as Element of REAL;
A13: f.2 >= 0 by A8,A11;
A14: 3 in dom f by A10,ENUMSET1:def 1;
  then
A15: f.3 = L.(F.3) by A8;
  then f/.3 = L.(F.3) by A14,PARTFUN1:def 6;
  then reconsider r3 = L.(F.3) as Element of REAL;
A16: f.3 >= 0 by A8,A14;
A17: 1 in dom f by A10,ENUMSET1:def 1;
  then
A18: f.1 = L.(F.1) by A8;
  then f/.1 = L.(F.1) by A17,PARTFUN1:def 6;
  then reconsider r1 = L.(F.1) as Element of REAL;
A19: f = <*r1,r2,r3*> by A9,A18,A12,A15,FINSEQ_1:45;
  then
A20: r1 + r2 + r3 = 1 by A7,RVSUM_1:78;
A21: f.1 >= 0 by A8,A17;
  ex a, b, c being Real st a = L.v1 & b = L.v2 & c = L.v3 & a + b
  + c = 1 & a >= 0 & b >= 0 & c >= 0
  proof
    per cases by A2,A3,A4,CONVEX1:31;
    suppose
A22:  F = <*v1,v2,v3*>;
      then
A23:  r1 = L.v1 & r2 = L.v2 by FINSEQ_1:45;
A24:  r2 >= 0 by A8,A11,A12;
A25:  r3 = L.v3 by A22,FINSEQ_1:45;
      r1 + r2 + r3 = 1 & r1 >= 0 by A7,A8,A17,A18,A19,RVSUM_1:78;
      hence thesis by A15,A16,A23,A25,A24;
    end;
    suppose
A26:  F = <*v1,v3,v2*>;
      then
A27:  r1 = L.v1 & r3 = L.v2 by FINSEQ_1:45;
A28:  r3 >= 0 by A8,A14,A15;
A29:  r2 = L.v3 by A26,FINSEQ_1:45;
      r1 + r3 + r2 = 1 & r1 >= 0 by A8,A17,A18,A20;
      hence thesis by A12,A13,A27,A29,A28;
    end;
    suppose
A30:  F = <*v2,v1,v3*>;
      then
A31:  r2 = L.v1 & r1 = L.v2 by FINSEQ_1:45;
A32:  r1 >= 0 by A8,A17,A18;
A33:  r3 = L.v3 by A30,FINSEQ_1:45;
      r2 + r1 + r3 = 1 & r2 >= 0 by A7,A8,A11,A12,A19,RVSUM_1:78;
      hence thesis by A15,A16,A31,A33,A32;
    end;
    suppose
A34:  F = <*v2,v3,v1*>;
      then
A35:  r3 = L.v1 & r1 = L.v2 by FINSEQ_1:45;
A36:  r1 >= 0 by A8,A17,A18;
A37:  r2 = L.v3 by A34,FINSEQ_1:45;
      r3 + r1 + r2 = 1 & r3 >= 0 by A8,A14,A15,A20;
      hence thesis by A12,A13,A35,A37,A36;
    end;
    suppose
A38:  F = <*v3,v1,v2*>;
      then
A39:  r2 = L.v1 & r3 = L.v2 by FINSEQ_1:45;
A40:  r3 >= 0 by A8,A14,A15;
A41:  r1 = L.v3 by A38,FINSEQ_1:45;
      r2 + r3 + r1 = 1 & r2 >= 0 by A8,A11,A12,A20;
      hence thesis by A18,A21,A39,A41,A40;
    end;
    suppose
A42:  F = <*v3,v2,v1*>;
      then
A43:  r3 = L.v1 & r2 = L.v2 by FINSEQ_1:45;
A44:  r2 >= 0 by A8,A11,A12;
A45:  r1 = L.v3 by A42,FINSEQ_1:45;
      r3 + r2 + r1 = 1 & r3 >= 0 by A8,A14,A15,A20;
      hence thesis by A18,A21,A43,A45,A44;
    end;
  end;
  hence thesis by A3,Lm3;
end;

theorem
  for V being ComplexLinearSpace, v being VECTOR of V, L being
C_Linear_Combination of {v} st L is convex holds ( ex r being Real st r = L.v &
  r = 1 ) & Sum L = L.v * v
proof
  let V be ComplexLinearSpace;
  let v be VECTOR of V;
  let L be C_Linear_Combination of {v};
  Carrier L c= {v} by Def4;
  then
A1: Carrier L = {} or Carrier L = {v} by ZFMISC_1:33;
  assume L is convex;
  hence thesis by A1,Th77,Th80;
end;

theorem
  for V being ComplexLinearSpace, v1,v2 being VECTOR of V, L being
  C_Linear_Combination of {v1,v2} st v1 <> v2 & L is convex holds ( ex r1, r2
being Real st r1 = L.v1 & r2 = L.v2 &r1 >= 0 & r2 >= 0 )& Sum L = L.v1 *
  v1 + L.v2 * v2
proof
  let V be ComplexLinearSpace;
  let v1,v2 be VECTOR of V;
  let L be C_Linear_Combination of {v1,v2};
  assume that
A1: v1 <> v2 and
A2: L is convex;
A3: Carrier L c= {v1,v2} by Def4;
A4: Carrier L <> {} by A2,Th77;
  ex r1, r2 being Real st r1 = L.v1 & r2 = L.v2 & r1 >= 0 & r2 >= 0
  proof
    per cases by A3,A4,ZFMISC_1:36;
    suppose
A5:   Carrier L = {v1};
      then not v2 in Carrier(L) by A1,TARSKI:def 1;
      then
A6:   0 = L.v2;
      ex r being Real st r = L.v1 & r = 1 by A2,A5,Th80;
      hence thesis by A6;
    end;
    suppose
A7:   Carrier L = {v2};
      then not v1 in Carrier L by A1,TARSKI:def 1;
      then
A8:   0=L.v1;
      ex r being Real st r =L.v2 & r = 1 by A2,A7,Th80;
      hence thesis by A8;
    end;
    suppose
      Carrier L = {v1,v2};
      then ex r1,r2 being Real st r1=L.v1 & r2 = L.v2 & r1 + r2 = 1 & r1 >= 0
      & r2 >=0 by A1,A2,Th81;
      hence thesis;
    end;
  end;
  hence thesis by A1,Th15;
end;

theorem
  for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V, L being
  C_Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is
convex holds ( ex r1, r2, r3 being Real st r1 = L.v1 & r2 = L.v2 & r3 =
L.v3 & r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = L.v1 * v1 + L
  .v2 * v2 + L.v3 * v3
proof
  let V be ComplexLinearSpace;
  let v1,v2,v3 be VECTOR of V;
  let L be C_Linear_Combination of {v1,v2,v3};
  assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1 and
A4: L is convex;
A5: Carrier L c= {v1,v2,v3} by Def4;
A6: Carrier L <> {} by A4,Th77;
  ex r1, r2, r3 being Real st r1 = L.v1 & r2 = L.v2 & r3 = L.v3 &
  r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0
  proof
    per cases by A5,A6,ZFMISC_1:118;
    suppose
A7:   Carrier L = {v1};
      then not v2 in Carrier L by A1,TARSKI:def 1;
      then
A8:   0 = L.v2;
A9:   1 + 0 + 0 =1;
      not v3 in Carrier L by A3,A7,TARSKI:def 1;
      then
A10:  0 = L.v3;
      ex r being Real st r = L.v1 & r = 1 by A4,A7,Th80;
      hence thesis by A8,A10,A9;
    end;
    suppose
A11:  Carrier L = {v2};
      then not v1 in Carrier L by A1,TARSKI:def 1;
      then
A12:  0 = L.v1;
A13:  0 + 1 + 0 =1;
      not v3 in Carrier L by A2,A11,TARSKI:def 1;
      then
A14:  0 = L.v3;
      ex r being Real st r = L.v2 & r = 1 by A4,A11,Th80;
      hence thesis by A12,A14,A13;
    end;
    suppose
A15:  Carrier L = {v3};
      then not v1 in Carrier L by A3,TARSKI:def 1;
      then
A16:  0 = L.v1;
A17:  0 + 0 + 1 =1;
      not v2 in Carrier L by A2,A15,TARSKI:def 1;
      then
A18:  0 = L.v2;
      ex r being Real st r = L.v3 & r = 1 by A4,A15,Th80;
      hence thesis by A16,A18,A17;
    end;
    suppose
A19:  Carrier L = {v1,v2};
      set r3 = 0;
      not v3 in {v where v is Element of V : L.v <> 0} by A2,A3,A19,
TARSKI:def 2;
      then
A20:  r3 = L.v3;
      consider r1, r2 being Real such that
A21:  r1 = L.v1 & r2 = L.v2 and
A22:  r1 + r2 = 1 and
A23:  r1 >= 0 & r2 >= 0 by A1,A4,A19,Th81;
      r1 + r2 + r3 = 1 by A22;
      hence thesis by A21,A23,A20;
    end;
    suppose
A24:  Carrier L = {v2,v3};
      set r1 = 0;
      not v1 in Carrier L by A1,A3,A24,TARSKI:def 2;
      then
A25:  r1 = L.v1;
      consider r2,r3 being Real such that
A26:  r2 = L.v2 & r3 = L.v3 and
A27:  r2 + r3 = 1 and
A28:  r2 >= 0 & r3 >= 0 by A2,A4,A24,Th81;
      r1 + r2 + r3 = 1 by A27;
      hence thesis by A26,A28,A25;
    end;
    suppose
A29:  Carrier L = {v1,v3};
      set r2 = 0;
      not v2 in Carrier(L) by A1,A2,A29,TARSKI:def 2;
      then
A30:  r2 = L.v2;
      consider r1, r3 being Real such that
A31:  r1 = L.v1 & r3 = L.v3 and
A32:  r1 + r3 = 1 and
A33:  r1 >= 0 & r3 >= 0 by A3,A4,A29,Th81;
      r1 + r2 + r3 = 1 by A32;
      hence thesis by A31,A33,A30;
    end;
    suppose
      Carrier L = {v1,v2,v3};
      hence thesis by A1,A2,A3,A4,Th82;
    end;
  end;
  hence thesis by A1,A2,A3,Lm3;
end;

begin  :: Complex Convex Hull

definition
  let V be non empty CLSStruct, M be Subset of V;
  func Convex-Family M -> Subset-Family of V means
  :Def25:
  for N being Subset of V holds N in it iff N is convex & M c= N;
  existence
  proof
    defpred P[Subset of V] means $1 is convex & M c= $1;
    thus ex F be Subset-Family of V st for N being Subset of V holds N in F
    iff P[N] from SUBSET_1:sch 3;
  end;
  uniqueness
  proof
    let SF,SG be Subset-Family of V;
    assume that
A1: for N being Subset of V holds N in SF iff N is convex & M c= N and
A2: for N being Subset of V holds N in SG iff N is convex & M c= N;
    for Y being Subset of V holds Y in SF iff Y in SG
    proof
      let Y be Subset of V;
      hereby
        assume Y in SF;
        then Y is convex & M c= Y by A1;
        hence Y in SG by A2;
      end;
      assume Y in SG;
      then Y is convex & M c= Y by A2;
      hence thesis by A1;
    end;
    hence thesis by SETFAM_1:31;
  end;
end;

definition
  let V be non empty CLSStruct, M be Subset of V;
  func conv M -> convex Subset of V equals
  meet (Convex-Family M);
  coherence
  proof
    for N being Subset of V st N in Convex-Family M holds N is convex by Def25;
    hence thesis by Th65;
  end;
end;

theorem
  for V being non empty CLSStruct, M being Subset of V, N being convex
  Subset of V st M c= N holds conv M c= N
proof
  let V be non empty CLSStruct;
  let M be Subset of V;
  let N be convex Subset of V;
  assume M c= N;
  then N in Convex-Family M by Def25;
  hence thesis by SETFAM_1:3;
end;