The Mizar article:

Some Properties for Convex Combinations

by
Noboru Endou,
Yasumasa Suzuki, and
Yasunari Shidama

Received April 3, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: CONVEX2
[ MML identifier index ]


environ

 vocabulary RLVECT_1, FUNCT_1, PROB_2, ARYTM_1, RELAT_1, BHSP_1, FINSEQ_1,
      BOOLE, JORDAN1, SETFAM_1, CONNSP_3, ARYTM_3, RLSUB_1, CONVEX1, FINSEQ_4,
      SEQ_1, CARD_1, RLVECT_2, JORDAN3, TARSKI, FUNCT_2, RFINSEQ, FINSET_1,
      CONVEX2;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
      FINSEQ_1, RELAT_1, FUNCT_1, FINSET_1, CARD_1, NAT_1, SETFAM_1, STRUCT_0,
      FUNCT_2, RLVECT_1, RLSUB_1, RLSUB_2, FINSEQ_4, RLVECT_2, RVSUM_1, BHSP_1,
      RUSUB_4, CONVEX1, TOPREAL1, JORDAN3, RFINSEQ;
 constructors REAL_1, SEQ_1, RUSUB_5, FINSEQ_4, CONVEX1, JORDAN3, NAT_1,
      MONOID_0, WELLORD2, TOPREAL1, MATRIX_2, RFINSEQ, RLSUB_2, MEMBERED;
 clusters RELSET_1, FINSEQ_1, ARYTM_3, STRUCT_0, RLVECT_1, SEQ_1, RUSUB_4,
      CONVEX1, BINARITH, XREAL_0, MEMBERED;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, CONVEX1;
 theorems BHSP_1, RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1,
      REAL_1, XBOOLE_0, REAL_2, SETFAM_1, AXIOMS, RLSUB_1, RUSUB_4, XBOOLE_1,
      RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, ENUMSET1, CONVEX1, PARTFUN1,
      JORDAN3, RLSUB_2, FUNCT_2, BINARITH, NAT_1, TOPREAL1, FVSUM_1, RFINSEQ,
      SQUARE_1, FINSET_1, VECTSP_9, PRALG_3, BAGORDER, EUCLID_2, INTEGRA5,
      XCMPLX_1;
 schemes BINARITH, RLVECT_4, XBOOLE_0, FINSEQ_1, FUNCT_1;

begin :: Convex Combination on Convex Family

theorem
  for V being non empty RLSStruct, M,N being convex Subset of V holds
 M /\ N is convex
proof
   let V be non empty RLSStruct;
   let M,N be convex Subset of V;
     let x,y be VECTOR of V;
     let r be Real;
     assume
A1:  0 < r & r < 1 & x in M /\ N & y in M /\ N;
     then x in M & x in N & y in M & y in N by XBOOLE_0:def 3;
     then r * x + (1-r) * y in M & r * x + (1-r) * y in N by A1,CONVEX1:def 2;
     hence thesis by XBOOLE_0:def 3;
end;

theorem
  for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
 F being FinSequence of the carrier of V, B being FinSequence of REAL st
  M = {u where u is VECTOR of V :
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u .|. v <= B.i}
    holds M is convex
proof
   let V be RealUnitarySpace-like (non empty UNITSTR);
   let M be Subset of V;
   let F be FinSequence of the carrier of V;
   let B be FinSequence of REAL;
   assume
A1:M = {u where u is VECTOR of V:
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u.|.v <= B.i};
     let u1,v1 be VECTOR of V;
     let r be Real;
     assume that
A2:  0 < r & r < 1 and
A3:  u1 in M & v1 in M;

     consider u' be VECTOR of V such that
A4:  u1 = u' and
A5:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & u'.|.v <= B.i by A1,A3;

     consider v' be VECTOR of V such that
A6:  v1 = v' and
A7:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & v'.|.v <= B.i by A1,A3;

       for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v <= B.i
     proof
       let i be Nat;
       assume
A8:    i in (dom F /\ dom B);
       then i in dom B by XBOOLE_0:def 3;
       then reconsider b = B.i as Real by PARTFUN1:27;

       consider x being VECTOR of V such that
A9:   x = F.i & u'.|. x <= b by A5,A8;
       consider y being VECTOR of V such that
A10:   y = F.i & v'.|. y <= b by A7,A8;

       take v = x;

A11:   r*(u1.|.v) <= r*b by A2,A4,A9,AXIOMS:25;

         0 + r < 1 by A2;
       then 1 - r > 0 by REAL_1:86;
then A12:   (1-r)*(v1.|.v) <= (1-r)*b by A6,A9,A10,AXIOMS:25;

         (r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
       then (r*u1 + (1-r)*v1).|.v <= r * b + (1-r)*(v1.|.v) by A11,AXIOMS:24;
       then (r*u1 + (1-r)*v1).|.v - r * b <= (1-r)*(v1.|.v) by REAL_1:86;
       then (r*u1 + (1-r)*v1).|.v - r * b <= (1-r)*b by A12,AXIOMS:22;
       then (r*u1 + (1-r)*v1).|.v <= r * b + (1-r)*b by REAL_1:86;
       then (r*u1 + (1-r)*v1).|.v <= (r+(1-r))*b by XCMPLX_1:8;
       then (r*u1 + (1-r)*v1).|.v <= (1+r-r)*b by XCMPLX_1:29;
       then (r*u1 + (1-r)*v1).|.v <= 1*b by XCMPLX_1:26;
       hence thesis by A9;
     end;
     hence r*u1 + (1-r)*v1 in M by A1;
end;

theorem
  for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
 F being FinSequence of the carrier of V, B being FinSequence of REAL st
  M = {u where u is VECTOR of V :
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u .|. v < B.i}
    holds M is convex
proof
   let V be RealUnitarySpace-like (non empty UNITSTR);
   let M be Subset of V;
   let F be FinSequence of the carrier of V;
   let B be FinSequence of REAL;
   assume
A1:M = {u where u is VECTOR of V:
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u.|.v < B.i};

     let u1,v1 be VECTOR of V;
     let r be Real;
     assume that
A2:  0 < r & r < 1 and
A3:  u1 in M & v1 in M;

     consider u' be VECTOR of V such that
A4:  u1 = u' and
A5:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & u'.|.v < B.i by A1,A3;

     consider v' be VECTOR of V such that
A6:  v1 = v' and
A7:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & v'.|.v < B.i by A1,A3;

       for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v < B.i
     proof
       let i be Nat;
       assume
A8:    i in (dom F /\ dom B);
       then i in dom B by XBOOLE_0:def 3;
       then reconsider b = B.i as Real by PARTFUN1:27;

       consider x being VECTOR of V such that
A9:   x = F.i & u'.|. x < b by A5,A8;
       consider y being VECTOR of V such that
A10:   y = F.i & v'.|. y < b by A7,A8;

       take v = x;

A11:   r*(u1.|.v) < r*b by A2,A4,A9,REAL_1:70;

         0 + r < 1 by A2;
       then 1 - r > 0 by REAL_1:86;
then A12:   (1-r)*(v1.|.v) <= (1-r)*b by A6,A9,A10,AXIOMS:25;

         (r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
       then (r*u1 + (1-r)*v1).|.v < r * b + (1-r)*(v1.|.v) by A11,REAL_1:67;
       then (r*u1 + (1-r)*v1).|.v - r * b < (1-r)*(v1.|.v) by REAL_1:84;
       then (r*u1 + (1-r)*v1).|.v - r * b < (1-r)*b by A12,AXIOMS:22;
       then (r*u1 + (1-r)*v1).|.v < r * b + (1-r)*b by REAL_1:84;
       then (r*u1 + (1-r)*v1).|.v < (r+(1-r))*b by XCMPLX_1:8;
       then (r*u1 + (1-r)*v1).|.v < (1+r-r)*b by XCMPLX_1:29;
       then (r*u1 + (1-r)*v1).|.v < 1*b by XCMPLX_1:26;
       hence thesis by A9;
     end;
     hence r*u1 + (1-r)*v1 in M by A1;
end;

theorem
  for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
 F being FinSequence of the carrier of V, B being FinSequence of REAL st
  M = {u where u is VECTOR of V :
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u .|. v >= B.i}
    holds M is convex
proof
   let V be RealUnitarySpace-like (non empty UNITSTR);
   let M be Subset of V;
   let F be FinSequence of the carrier of V;
   let B be FinSequence of REAL;
   assume
A1:M = {u where u is VECTOR of V:
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u.|.v >= B.i};

     let u1,v1 be VECTOR of V;
     let r be Real;
     assume that
A2:  0 < r & r < 1 and
A3:  u1 in M & v1 in M;

     consider u' be VECTOR of V such that
A4:  u1 = u' and
A5:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & u'.|.v >= B.i by A1,A3;

     consider v' be VECTOR of V such that
A6:  v1 = v' and
A7:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & v'.|.v >= B.i by A1,A3;

       for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v >= B.i
     proof
       let i be Nat;
       assume
A8:    i in (dom F /\ dom B);
       then i in dom B by XBOOLE_0:def 3;
       then reconsider b = B.i as Real by PARTFUN1:27;

       consider x being VECTOR of V such that
A9:   x = F.i & u'.|. x >= b by A5,A8;
       consider y being VECTOR of V such that
A10:   y = F.i & v'.|. y >= b by A7,A8;

       take v = x;

A11:   r*(u1.|.v) >= r*b by A2,A4,A9,AXIOMS:25;

         0 + r < 1 by A2;
       then 1 - r > 0 by REAL_1:86;
then A12:   (1-r)*(v1.|.v) >= (1-r)*b by A6,A9,A10,AXIOMS:25;

         (r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
       then (r*u1 + (1-r)*v1).|.v >= r * b + (1-r)*(v1.|.v) by A11,AXIOMS:24;
       then (r*u1 + (1-r)*v1).|.v - r * b >= (1-r)*(v1.|.v) by REAL_1:84;
       then (r*u1 + (1-r)*v1).|.v - r * b >= (1-r)*b by A12,AXIOMS:22;
       then (r*u1 + (1-r)*v1).|.v >= r * b + (1-r)*b by REAL_1:84;
       then (r*u1 + (1-r)*v1).|.v >= (r+(1-r))*b by XCMPLX_1:8;
       then (r*u1 + (1-r)*v1).|.v >= (1+r-r)*b by XCMPLX_1:29;
       then (r*u1 + (1-r)*v1).|.v >= 1*b by XCMPLX_1:26;
       hence thesis by A9;
     end;
     hence r*u1 + (1-r)*v1 in M by A1;
end;

theorem
  for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
 F being FinSequence of the carrier of V, B being FinSequence of REAL st
  M = {u where u is VECTOR of V :
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u .|. v > B.i}
    holds M is convex
proof
   let V be RealUnitarySpace-like (non empty UNITSTR);
   let M be Subset of V;
   let F be FinSequence of the carrier of V;
   let B be FinSequence of REAL;
   assume
A1:M = {u where u is VECTOR of V:
        for i being Nat st i in (dom F /\ dom B) holds
         ex v being VECTOR of V st v = F.i & u.|.v > B.i};

     let u1,v1 be VECTOR of V;
     let r be Real;
     assume that
A2:  0 < r & r < 1 and
A3:  u1 in M & v1 in M;

     consider u' be VECTOR of V such that
A4:  u1 = u' and
A5:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & u'.|.v > B.i by A1,A3;

     consider v' be VECTOR of V such that
A6:  v1 = v' and
A7:  for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & v'.|.v > B.i by A1,A3;

       for i being Nat st i in (dom F /\ dom B) holds
      ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v > B.i
     proof
       let i be Nat;
       assume
A8:    i in (dom F /\ dom B);
       then i in dom B by XBOOLE_0:def 3;
       then reconsider b = B.i as Real by PARTFUN1:27;

       consider x being VECTOR of V such that
A9:   x = F.i & u'.|. x > b by A5,A8;
       consider y being VECTOR of V such that
A10:   y = F.i & v'.|. y > b by A7,A8;

       take v = x;

A11:   r*(u1.|.v) > r*b by A2,A4,A9,REAL_1:70;

         0 + r < 1 by A2;
       then 1 - r > 0 by REAL_1:86;
then A12:   (1-r)*(v1.|.v) >= (1-r)*b by A6,A9,A10,AXIOMS:25;

         (r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
        .= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
       then (r*u1 + (1-r)*v1).|.v > r * b + (1-r)*(v1.|.v) by A11,REAL_1:67;
       then (r*u1 + (1-r)*v1).|.v - r * b > (1-r)*(v1.|.v) by REAL_1:86;
       then (r*u1 + (1-r)*v1).|.v - r * b > (1-r)*b by A12,AXIOMS:22;
       then (r*u1 + (1-r)*v1).|.v > r * b + (1-r)*b by REAL_1:86;
       then (r*u1 + (1-r)*v1).|.v > (r+(1-r))*b by XCMPLX_1:8;
       then (r*u1 + (1-r)*v1).|.v > (1+r-r)*b by XCMPLX_1:29;
       then (r*u1 + (1-r)*v1).|.v > 1*b by XCMPLX_1:26;
       hence thesis by A9;
     end;
     hence r*u1 + (1-r)*v1 in M by A1;
end;

Lm1:
for V being RealLinearSpace, M being convex Subset of V holds
 for N being Subset of V, L being Linear_Combination of N st
  L is convex & N c= M holds Sum(L) in M
proof
   let V be RealLinearSpace;
   let M be convex Subset of V;
   let N be Subset of V;
   let L be Linear_Combination of N;
   assume that
A1:L is convex and
A2:N c= M;

   consider F being FinSequence of the carrier of V such that
A3:F is one-to-one and
A4:rng F = Carrier L and
A5:ex f being FinSequence of REAL st len f = len F & Sum(f) = 1 &
    (for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0)
     by A1,CONVEX1:def 3;
   consider f being FinSequence of REAL such that
A6:len f = len F and
A7:Sum(f) = 1 and
A8:for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;

A9:len F >= 1
   proof
       Carrier(L) <> {} by A1,CONVEX1:21;
     then not (Carrier(L),{} are_equipotent) by CARD_1:46;
     then card(Carrier(L)) <> card {} by CARD_1:21;
     then len F <> card {} by A3,A4,FINSEQ_4:77;
     then len F > 0 by CARD_1:78,NAT_1:19;
     then len F >= 0 + 1 by NAT_1:38;
     hence thesis;
   end;
   then len F in Seg len F by FINSEQ_1:3;
   then reconsider i = len F as non empty Nat by BINARITH:5;

   defpred P[Nat] means
    (1/Sum(mid(f,1,$1)))*Sum(mid(L(#)F,1,$1)) in M;

A10:len (L(#)F) = len F by RLVECT_2:def 9;

A11:P[1]
   proof
       mid(f,1,1) = f|1 by JORDAN3:25;
then A12: len(mid(f,1,1)) = 1 by A6,A9,TOPREAL1:3;
     then 1 in dom mid(f,1,1) by FINSEQ_3:27;
     then reconsider m = mid(f,1,1).1 as Element of REAL by PARTFUN1:27;
       mid(f,1,1)= <* mid(f,1,1).1 *> by A12,FINSEQ_1:57;
then A13: Sum(mid(f,1,1)) = m by RVSUM_1:103;
       mid(L(#)F,1,1) = (L(#)F)|1 by JORDAN3:25;
then A14: len(mid(L(#)F,1,1)) = 1 by A9,A10,TOPREAL1:3;
       1 in Seg len (L(#)F) by A9,A10,FINSEQ_1:3;
then A15: 1 in dom (L(#)F) & 1 in dom F & 1 in dom f by A6,A10,FINSEQ_1:def 3;
then A16: F/.1 = F.1 by FINSEQ_4:def 4;
A17: mid(L(#)F,1,1).1 = (L(#)F).1 by A9,A10,JORDAN3:32
      .=L.(F/.1)*F/.1 by A15,RLVECT_2:def 9;
       f.1 = L.(F.1) by A8,A15 .= L.(F/.1) by A15,FINSEQ_4:def 4;
then A18: Sum(mid(f,1,1)) = L.(F/.1) by A6,A9,A13,JORDAN3:32;
A19: F.1 in rng F by A15,FUNCT_1:def 5;
     then F.1 in {v where v is Element of V : L.v <> 0}
      by A4,RLVECT_2:def 6;
     then consider v2 being Element of V such that
A20: F.1 = v2 & L.v2 <> 0;

       mid(L(#)F,1,1) = <* mid(L(#)F,1,1).1 *> by A14,FINSEQ_1:57;
then A21: (1/Sum(mid(f,1,1)))*Sum(mid(L(#)F,1,1))
      = (1/Sum(mid(f,1,1))) * (L.(F/.1) * F/.1) by A17,RLVECT_1:61
     .= ((1/Sum(mid(f,1,1))) * L.(F/.1)) * F/.1 by RLVECT_1:def 9
     .= 1 * F/.1 by A16,A18,A20,XCMPLX_1:107
     .= F/.1 by RLVECT_1:def 9;
       Carrier(L) c= N by RLVECT_2:def 8;
     then Carrier(L) c= M by A2,XBOOLE_1:1;
     hence thesis by A4,A16,A19,A21;
   end;

A22:for k being non empty Nat st P[k] holds P[k+1]
   proof
     let k be non empty Nat;
     assume
A23: (1/Sum(mid(f,1,k)))*Sum(mid(L(#)F,1,k)) in M;
A24: k >= 1 by RLVECT_1:99;
       now per cases;
       suppose
A25:   k >= len f;

A26:   mid(f,1,k) = f|k by A24,JORDAN3:25 .= f by A25,TOPREAL1:2;

A27:   mid(L(#)F,1,k) = (L(#)F)|k by A24,JORDAN3:25 .= L(#)F
         by A6,A10,A25,TOPREAL1:2;

A28:   k+1 >= 1 & k+1 >= len f & k+1 >= len (L(#)F)
        by A6,A10,A25,NAT_1:37;
then A29:   mid(f,1,k+1) = f|(k+1) by JORDAN3:25 .= f by A28,TOPREAL1:2;
         mid(L(#)F,1,k+1) = (L(#)F)|(k+1) by A28,JORDAN3:25
        .= L(#)F by A28,TOPREAL1:2;
       hence thesis by A23,A26,A27,A29;

       suppose
A30:   k < len f;
then A31:   k+1 >= 1 & k+1 <= len f by A24,NAT_1:38;

         mid(f,1,k) = f|k by A24,JORDAN3:25;
then A32:   len mid(f,1,k) = k by A30,TOPREAL1:3;
A33:   len <* mid(f,1,k+1).(k+1) *> = 1 by FINSEQ_1:57;

         mid(f,1,k+1) = f|(k+1) by A31,JORDAN3:25;
       then len mid(f,1,k+1) = k+1 by A31,TOPREAL1:3;
then A34:   dom mid(f,1,k+1) = Seg (len mid(f,1,k) + len <* mid(f,1,k+1).(k+1)
*>)
        by A32,A33,FINSEQ_1:def 3;

A35:   mid(f,1,k+1) = f|(k+1) by A31,JORDAN3:25;
A36:   len (f|(k+1)) = k+1 by A31,TOPREAL1:3;

A37:   for i being Nat st i in dom mid(f,1,k) holds
        mid(f,1,k+1).i = mid(f,1,k).i
       proof
         let i be Nat;
         assume
A38:     i in dom mid(f,1,k);
A39:     mid(f,1,k) = f|k by A24,JORDAN3:25;
         then (f|k).i = (f|k)/.i by A38,FINSEQ_4:def 4;
then A40:     mid(f,1,k).i = f/.i by A38,A39,TOPREAL1:1;

A41:     i in Seg len(f|k) by A38,A39,FINSEQ_1:def 3;
           len(f|k) = k by A30,TOPREAL1:3;
         then 1 <= i & i <= k by A41,FINSEQ_1:3;
         then 1 <= i & i <= k+1 by NAT_1:37;
         then i in Seg (k+1) by FINSEQ_1:3;
then A42:     i in dom (f|(k+1)) by A36,FINSEQ_1:def 3;
         then (f|(k+1)).i = (f|(k+1))/.i by FINSEQ_4:def 4;
         hence thesis by A35,A40,A42,TOPREAL1:1;
       end;

    for i being Nat st i in dom <* mid(f,1,k+1).(k+1) *> holds
        mid(f,1,k+1).(len mid(f,1,k) + i) = <* mid(f,1,k+1).(k+1) *>.i
       proof
         let i be Nat;
         assume
           i in dom <* mid(f,1,k+1).(k+1) *>;
         then i in Seg 1 by FINSEQ_1:55;
         then i = 1 by FINSEQ_1:4,TARSKI:def 1;
         hence thesis by A32,FINSEQ_1:57;
       end;

then A43:   mid(f,1,k+1)=mid(f,1,k)^<* mid(f,1,k+1).(k+1) *>
        by A34,A37,FINSEQ_1:def 7;

         k+1 in Seg (k+1) by A31,FINSEQ_1:3;
then A44:   k+1 in dom (f|(k+1)) by A36,FINSEQ_1:def 3;
       then (f|(k+1))/.(k+1) = f/.(k+1) by TOPREAL1:1;
then A45:   mid(f,1,k+1).(k+1) = f/.(k+1) by A35,A44,FINSEQ_4:def 4;

A46:   k+1 in Seg len f by A31,FINSEQ_1:3;
then A47:   k+1 in dom f by FINSEQ_1:def 3;
then A48:   mid(f,1,k+1).(k+1) = f.(k+1) by A45,FINSEQ_4:def 4
        .= L.(F.(k+1)) by A8,A47;

         k+1 in dom F by A6,A46,FINSEQ_1:def 3;
       then mid(f,1,k+1).(k+1) = L.(F/.(k+1)) by A48,FINSEQ_4:def 4;
then A49:   Sum(mid(f,1,k+1)) = Sum(mid(f,1,k)) + L.(F/.(k+1)) by A43,RVSUM_1:
104;

A50:   k < len (L(#)F) by A6,A30,RLVECT_2:def 9;
then A51:   k+1 >= 1 & k+1 <= len (L(#)F) by A24,NAT_1:38;

         mid(L(#)F,1,k) = (L(#)F)|k by A24,JORDAN3:25;
then A52:   len mid(L(#)F,1,k) = k by A50,TOPREAL1:3;
A53:   len <* mid(L(#)F,1,k+1).(k+1) *> = 1 by FINSEQ_1:57;
A54:   mid(L(#)F,1,k+1) = (L(#)F)|(k+1) by A51,JORDAN3:25;
       then len mid(L(#)F,1,k+1) = k+1 by A51,TOPREAL1:3;
then A55:   dom mid(L(#)F,1,k+1)
        = Seg (len mid(L(#)F,1,k) + len <* mid(L(#)F,1,k+1).(k+1) *>)
        by A52,A53,FINSEQ_1:def 3;

A56:   len ((L(#)F)|(k+1)) = k+1 by A51,TOPREAL1:3;

A57:   for i being Nat st i in dom mid(L(#)F,1,k) holds
        mid(L(#)F,1,k+1).i = mid(L(#)F,1,k).i
       proof
         let i be Nat;
         assume
A58:     i in dom mid(L(#)F,1,k);
A59:     mid(L(#)F,1,k) = (L(#)F)|k by A24,JORDAN3:25;
         then ((L(#)F)|k).i = ((L(#)F)|k)/.i by A58,FINSEQ_4:def 4;
then A60:     mid(L(#)F,1,k).i = (L(#)F)/.i by A58,A59,TOPREAL1:1;

A61:     i in Seg len((L(#)F)|k) by A58,A59,FINSEQ_1:def 3;
           len((L(#)F)|k) = k by A50,TOPREAL1:3;
         then 1 <= i & i <= k by A61,FINSEQ_1:3;
         then 1 <= i & i <= k+1 by NAT_1:37;
         then i in Seg (k+1) by FINSEQ_1:3;
then A62:     i in dom ((L(#)F)|(k+1)) by A56,FINSEQ_1:def 3;
         then ((L(#)F)|(k+1)).i = ((L(#)F)|(k+1))/.i by FINSEQ_4:def 4;
         hence thesis by A54,A60,A62,TOPREAL1:1;
       end;

         for i being Nat st i in dom <* mid(L(#)F,1,k+1).(k+1) *> holds
        mid(L(#)F,1,k+1).(len mid(L(#)F,1,k) + i)
         = <* mid(L(#)F,1,k+1).(k+1) *>.i
       proof
         let i be Nat;
         assume
           i in dom <* mid(L(#)F,1,k+1).(k+1) *>;
         then i in Seg 1 by FINSEQ_1:55;
         then i = 1 by FINSEQ_1:4,TARSKI:def 1;
         hence thesis by A52,FINSEQ_1:57;
       end;

then A63:   mid(L(#)F,1,k+1) = mid(L(#)F,1,k)^<* mid(L(#)F,1,k+1).(k+1) *>
         by A55,A57,FINSEQ_1:def 7;

         k+1 in Seg (k+1) by A31,FINSEQ_1:3;
then A64:   k+1 in dom ((L(#)F)|(k+1)) by A56,FINSEQ_1:def 3;
       then ((L(#)F)|(k+1))/.(k+1) = (L(#)F)/.(k+1) by TOPREAL1:1;
then A65:   mid((L(#)F),1,k+1).(k+1) = (L(#)F)/.(k+1) by A54,A64,FINSEQ_4:def 4
;

         k+1 <= len (L(#)F) by A6,A31,RLVECT_2:def 9;
then A66:   k+1 in dom (L(#)F) by A31,FINSEQ_3:27;
then A67:   mid((L(#)F),1,k+1).(k+1) = (L(#)F).(k+1) by A65,FINSEQ_4:def 4
        .= L.(F/.(k+1)) * F/.(k+1) by A66,RLVECT_2:def 9;

       set r1 = Sum(mid(f,1,k));
       set r2 = L.(F/.(k+1));
       set w1 = Sum(mid(L(#)F,1,k));
       set w2 = F/.(k+1);

A68:    for i being Nat st i in dom mid(f,1,k) holds 0 <= mid(f,1,k).i
       proof
         let i be Nat;
         assume i in dom mid(f,1,k);
         then i in Seg k by A32,FINSEQ_1:def 3;
then A69:      1 <= i & i <= k by FINSEQ_1:3;
then A70:      mid(f,1,k).i = f.i by A30,JORDAN3:32;
           1 <= i & i <= len f by A30,A69,AXIOMS:22;
         then i in dom f by FINSEQ_3:27;
         hence thesis by A8,A70;
       end;

         ex i being Nat st i in dom mid(f,1,k) & 0 < mid(f,1,k).i
       proof
A71:      1 in Seg len mid(f,1,k) by A24,A32,FINSEQ_1:3;
           1 <= len f by A24,A30,AXIOMS:22;
then A72:      1 in Seg len f by FINSEQ_1:3;
         then 1 in dom f by FINSEQ_1:def 3;
then A73:      f.1 = L.(F.1) & f.1 >= 0 by A8;
           1 in dom F by A6,A72,FINSEQ_1:def 3;
         then F.1 in Carrier(L) by A4,FUNCT_1:def 5;
         then F.1 in {v where v is Element of V : L.v <> 0}
           by RLVECT_2:def 6;
         then consider v being Element of V such that
A74:      v = F.1 & L.v <> 0;
         take 1;
         thus thesis by A24,A30,A71,A73,A74,FINSEQ_1:def 3,JORDAN3:32;
       end;

then A75:    r1 > 0 by A68,RVSUM_1:115;

A76:    w2 in M & r2 > 0
       proof
           k+1 in Seg len F by A6,A31,FINSEQ_1:3;
then A77:      k+1 in dom F by FINSEQ_1:def 3;
         then w2 = F.(k+1) by FINSEQ_4:def 4;
then A78:      w2 in Carrier(L) by A4,A77,FUNCT_1:def 5;
           Carrier(L) c= N by RLVECT_2:def 8;
         hence w2 in M by A2,A78,TARSKI:def 3;
           w2 in {v where v is Element of V : L.v <> 0}
           by A78,RLVECT_2:def 6;
         then consider v being Element of V such that
A79:      v = w2 & L.v <> 0;
           k+1 in Seg len f by A31,FINSEQ_1:3;
         then k+1 in dom f by FINSEQ_1:def 3;
         then f.(k+1) = L.(F.(k+1)) & f.(k+1) >= 0 by A8;
         hence r2 > 0 by A77,A79,FINSEQ_4:def 4;
       end;

then A80:    r1+r2 > 0+0 by A75,REAL_1:67;

A81:    0 < (1/(r1+r2))*r1 & (1/(r1+r2))*r1 < 1
       proof
           1/(r1+r2) > 0 by A80,REAL_2:127;
         hence (1/(r1+r2))*r1 > 0 by A75,REAL_2:122;

A82:      r1+r2 > r1 by A76,REAL_1:69;
           (1/(r1+r2))*r1 = r1/(r1+r2) by XCMPLX_1:100;
         hence (1/(r1+r2))*r1 < 1 by A75,A82,REAL_2:142;
       end;

A83:    (1/(r1+r2))*r2 = 1 - (1/(r1+r2))*r1
       proof
           1 - (1/(r1+r2))*r1 = (r1+r2)*(1/(r1+r2)) - (1/(r1+r2))*r1
          by A80,XCMPLX_1:107
          .= (r1+r2-r1)*(1/(r1+r2)) by XCMPLX_1:40;
         hence thesis by XCMPLX_1:26;
       end;

         (1/Sum(mid(f,1,k+1)))*Sum(mid(L(#)F,1,k+1))
        = (1/(r1+r2))*(w1+r2*w2) by A49,A63,A67,FVSUM_1:87
       .= (1/(r1+r2))*(1 * w1 + r2 * w2) by RLVECT_1:def 9
       .= (1/(r1+r2))*((r1 * (1/r1)) * w1 + r2 * w2) by A75,XCMPLX_1:107
       .= (1/(r1+r2))*(r1 * ((1/r1)*w1) + r2 * w2) by RLVECT_1:def 9
       .= (1/(r1+r2))*(r1 * ((1/r1)*w1))
         +(1/(r1+r2))*(r2 * w2) by RLVECT_1:def 9
       .= (1/(r1+r2))*r1 * ((1/r1)*w1)
         +(1/(r1+r2))*(r2 * w2) by RLVECT_1:def 9
       .= (1/(r1+r2))*r1 * ((1/r1)*w1)
         +(1/(r1+r2))*r2 * w2 by RLVECT_1:def 9;
       hence thesis by A23,A76,A81,A83,CONVEX1:def 2;
     end;
     hence thesis;
   end;
     for k being non empty Nat holds P[k] from Ind_from_1(A11,A22);
then A84:(1/Sum(mid(f,1,i)))*Sum(mid(L(#)F,1,i)) in M;
A85:len (L (#) F) = len F by RLVECT_2:def 9;
     Sum(mid(f,1,len f)) = 1 by A6,A7,A9,JORDAN3:29;
   then (1/Sum(mid(f,1,len f)))*Sum(mid(L(#)F,1,len(L(#)F)))
    = Sum(mid(L(#)F,1,len(L(#)F))) by RLVECT_1:def 9
   .= Sum(L (#) F) by A9,A85,JORDAN3:29;
   hence thesis by A3,A4,A6,A84,A85,RLVECT_2:def 10;
end;

Lm2:
for V being RealLinearSpace, M being Subset of V st
 for N being Subset of V, L being Linear_Combination of N st
  L is convex & N c= M holds Sum(L) in M
   holds M is convex
proof
   let V be RealLinearSpace;
   let M be Subset of V;
   assume
A1:for N being Subset of V, L being Linear_Combination of N st
    L is convex & N c= M holds Sum(L) in M;

     let u,v be VECTOR of V;
     let r be Real;
     assume that
A2:  0 < r and
A3:  r < 1 and
A4:  u in M and
A5:  v in M;
     set N = {u,v};
A6:  N c= M by A4,A5,ZFMISC_1:38;
     reconsider N as Subset of V;

       now per cases;
      suppose A7:u <> v;
      consider L being Linear_Combination of {u,v} such that
A8:   L.u = r & L.v = (1-r) from LinCEx2(A7);
      reconsider L as Linear_Combination of N;
A9:   Sum(L)=r*u + (1-r)*v by A7,A8,RLVECT_2:51;
        L is convex
      proof
          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)))
        proof
A10:       Carrier L c= {u,v} by RLVECT_2:def 8;
            u in {w where w is Element of V : L.w <> 0}
            by A2,A8;
then A11:       u in Carrier L by RLVECT_2:def 6;
            r-r < 1-r by A3,REAL_1:54;
then A12:      0 < 1-r by XCMPLX_1:14;
          then v in {w where w is Element of V : L.w <> 0}
            by A8;
          then v in Carrier L by RLVECT_2:def 6;
then A13:       {u,v} c= Carrier L by A11,ZFMISC_1:38;
            <*u,v*> = <*u*>^<*v*> by FINSEQ_1:def 9;
then A14:       rng <*u,v*> = rng <*u*> \/ rng <*v*> by FINSEQ_1:44
           .= {u} \/ rng <*v*> by FINSEQ_1:55
           .= {u} \/ {v} by FINSEQ_1:55
           .= {u,v} by ENUMSET1:41
           .= Carrier L by A10,A13,XBOOLE_0:def 10;
A15:       ex f being FinSequence of REAL st len f = len <*u,v*> & Sum(f) = 1 &
          (for n being Nat st n in dom f holds f.n = L.(<*u,v*>.n) & f.n >= 0)
          proof
A16:         len <*r,1-r*> = 2 by FINSEQ_1:61 .= len <*u,v*> by FINSEQ_1:61;
A17:         Sum(<*r,1-r*>) = r + (1-r) by RVSUM_1:107
             .= r + 1 - r by XCMPLX_1:29 .= 1 by XCMPLX_1:26;
A18:         for n being Nat st n in dom <*r,1-r*>
             holds <*r,1-r*>.n = L.(<*u,v*>.n) & <*r,1-r*>.n >= 0
            proof
              let n be Nat;
              assume n in dom <*r,1-r*>;
              then n in Seg len <*r,1-r*> by FINSEQ_1:def 3;
then A19:          n in {1,2} by FINSEQ_1:4,61;
                now per cases by A19,TARSKI:def 2;
                suppose
A20:            n = 1;
                then L.(<*u,v*>.n) = r by A8,FINSEQ_1:61;
                hence thesis by A2,A20,FINSEQ_1:61;
                suppose
A21:            n = 2;
                then L.(<*u,v*>.n) = 1-r by A8,FINSEQ_1:61;
                hence thesis by A12,A21,FINSEQ_1:61;
              end;
              hence thesis;
            end;
            take <*r,1-r*>;
            thus thesis by A16,A17,A18;
          end;
          take <*u,v*>;
          thus thesis by A7,A14,A15,FINSEQ_3:103;
        end;
        hence thesis by CONVEX1:def 3;
      end;
      hence thesis by A1,A6,A9;

      suppose A22:u = v;
      consider L being Linear_Combination of {u} such that
A23:  L.u = 1 from LinCEx1;
      reconsider L as Linear_Combination of N by A22,ENUMSET1:69;
        L is convex
      proof
          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)))
        proof
A24:       Carrier L c= {u,v} by RLVECT_2:def 8;
            u in {w where w is Element of V : L.w <> 0}
            by A23;
then A25:       u in Carrier L by RLVECT_2:def 6;
            v in {w where w is Element of V : L.w <> 0}
            by A22,A23;
          then v in Carrier L by RLVECT_2:def 6;
          then {u,v} c= Carrier L by A25,ZFMISC_1:38;
          then Carrier L = {u,v} by A24,XBOOLE_0:def 10;
then A26:       Carrier L = {u} by A22,ENUMSET1:69;

A27:      ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 &
           for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
          proof
            reconsider f = <*1*> as FinSequence of REAL;
A28:         len <*1*> = 1 by FINSEQ_1:56 .= len <*u*> by FINSEQ_1:56;
A29:        for n being Nat st n in dom f holds f.n = L.(<*u*>.n) &
             f.n >= 0
            proof
              let n be Nat;
              assume n in dom f;
              then n in {1} by FINSEQ_1:4,55;
then A30:           n = 1 by TARSKI:def 1;
then A31:           f.n = 1 by FINSEQ_1:57
              .= L.(<*u*>.n) by A23,A30,FINSEQ_1:57;
                f.n = 1 by A30,FINSEQ_1:57;
              hence thesis by A31;
            end;
            take f;
            thus thesis by A28,A29,RVSUM_1:103;
          end;
          take <*u*>;
          thus thesis by A26,A27,FINSEQ_1:55,FINSEQ_3:102;
        end;
        hence thesis by CONVEX1:def 3;
      end;
then A32:  Sum(L) in M by A1,A6;
        r*u + (1-r)*v = (r+(1-r))*u by A22,RLVECT_1:def 9
      .= (r+1-r)*u by XCMPLX_1:29
      .= (r-r+1)*u by XCMPLX_1:29
      .= (0+1)*u by XCMPLX_1:14;
      hence thesis by A23,A32,RLVECT_2:50;
     end;
     hence thesis;
end;

theorem
  for V being RealLinearSpace, M being Subset of V holds
 (for N being Subset of V, L being Linear_Combination of N st
  L is convex & N c= M holds Sum(L) in M)
   iff M is convex by Lm1,Lm2;

definition let V be RealLinearSpace, M be Subset of V;
  defpred P[set] means $1 is Linear_Combination of M;
 func LinComb(M) -> set means
   for L being set holds
  L in it iff L is Linear_Combination of M;
existence
proof
   consider A being set such that
A1: for x being set holds
     x in A iff x in Funcs(the carrier of V, REAL) & P[x] from Separation;
   take A;
   let L be set;
   thus L in A implies L is Linear_Combination of M by A1;
   assume L is Linear_Combination of M;
   hence thesis by A1;
  end;
uniqueness
  proof
   thus for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
  end;
end;

Lm3:
for V being RealLinearSpace holds
 ex L be Linear_Combination of V st L is convex
proof
   let V be RealLinearSpace;
   consider u being Element of V;
   consider L being Linear_Combination of {u} such that
A1:L.u = 1 from LinCEx1;
     reconsider L as Linear_Combination of V;
A2:  L is convex
     proof
A3:      Carrier L c= {u} by RLVECT_2:def 8;
           u in {w where w is Element of V : L.w <> 0}
           by A1;
         then u in Carrier L by RLVECT_2:def 6;
         then {u} c= Carrier L by ZFMISC_1:37;
then A4:      Carrier L = {u} by A3,XBOOLE_0:def 10;

A5:     ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 &
          for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
         proof
           reconsider f = <*1*> as FinSequence of REAL;
A6:        len <*1*> = 1 by FINSEQ_1:56 .= len <*u*> by FINSEQ_1:56;
A7:       for n being Nat st n in dom f holds f.n = L.(<*u*>.n) &
            f.n >= 0
           proof
             let n be Nat;
             assume n in dom f;
             then n in {1} by FINSEQ_1:4,55;
then A8:          n = 1 by TARSKI:def 1;
then A9:          f.n = L.u by A1,FINSEQ_1:57
             .= L.(<*u*>.n) by A8,FINSEQ_1:57;
               f.n = 1 by A8,FINSEQ_1:57;
             hence thesis by A9;
           end;
           take f;
           thus thesis by A6,A7,RVSUM_1:103;
         end;
         take <*u*>;
         thus thesis by A4,A5,FINSEQ_1:55,FINSEQ_3:102;
     end;
     take L;
     thus thesis by A2;
end;

definition let V be RealLinearSpace;
 cluster convex Linear_Combination of V;
existence by Lm3;
end;

definition let V be RealLinearSpace;
 mode Convex_Combination of V is convex Linear_Combination of V;
end;

Lm4:
for V being RealLinearSpace, M being non empty Subset of V holds
 ex L being Linear_Combination of M st L is convex
proof
   let V be RealLinearSpace;
   let M be non empty Subset of V;
   consider u being set such that
A1:u in M by XBOOLE_0:def 1;
   reconsider u as Element of V by A1;
   consider L being Linear_Combination of {u} such that
A2:L.u = 1 from LinCEx1;
       {u} c= M by A1,ZFMISC_1:37;
     then reconsider L as Linear_Combination of M by RLVECT_2:33;
A3:  L is convex
     proof
A4:      Carrier L c= {u} by RLVECT_2:def 8;
           u in {w where w is Element of V : L.w <> 0}
           by A2;
         then u in Carrier L by RLVECT_2:def 6;
         then {u} c= Carrier L by ZFMISC_1:37;
then A5:      Carrier L = {u} by A4,XBOOLE_0:def 10;

A6:     ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 &
          for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
         proof
           reconsider f = <*1*> as FinSequence of REAL;
A7:        len <*1*> = 1 by FINSEQ_1:56 .= len <*u*> by FINSEQ_1:56;
A8:       for n being Nat st n in dom f holds f.n = L.(<*u*>.n) &
            f.n >= 0
           proof
             let n be Nat;
             assume n in dom f;
             then n in {1} by FINSEQ_1:4,55;
then A9:          n = 1 by TARSKI:def 1;
then A10:          f.n = L.u by A2,FINSEQ_1:57
             .= L.(<*u*>.n) by A9,FINSEQ_1:57;
               f.n = 1 by A9,FINSEQ_1:57;
             hence thesis by A10;
           end;
           take f;
           thus thesis by A7,A8,RVSUM_1:103;
         end;
         take <*u*>;
         thus thesis by A5,A6,FINSEQ_1:55,FINSEQ_3:102;
     end;
     take L;
     thus thesis by A3;
end;

definition let V be RealLinearSpace, M be non empty Subset of V;
 cluster convex Linear_Combination of M;
existence by Lm4;
end;

definition let V be RealLinearSpace, M be non empty Subset of V;
 mode Convex_Combination of M is convex Linear_Combination of M;
end;

Lm5:
for V being RealLinearSpace, W1,W2 being Subspace of V holds
 Up(W1+W2) = Up(W1) + Up(W2)
proof
   let V be RealLinearSpace;
   let W1,W2 being Subspace of V;
A1:Up(W1+W2) = the carrier of W1+W2 by RUSUB_4:def 6
    .= {v + u where v,u is VECTOR of V : v in W1 & u in W2} by RLSUB_2:def 1;
     for x being set st x in Up(W1+W2) holds x in Up(W1) + Up(W2)
   proof
     let x be set;
     assume x in Up(W1+W2);
     then consider v,u being VECTOR of V such that
A2:  x = v + u & v in W1 & u in W2 by A1;
       v in the carrier of W1 & u in the carrier of W2 by A2,RLVECT_1:def 1;
     then v in Up(W1) & u in Up(W2) by RUSUB_4:def 6;
     then x in {u' + v' where u',v' is Element of V:
      u' in Up(W1) & v' in Up(W2)} by A2;
     hence thesis by RUSUB_4:def 10;
   end;
then A3:Up(W1+W2) c= Up(W1) + Up(W2) by TARSKI:def 3;
     for x being set st x in Up(W1) + Up(W2) holds x in Up(W1+W2)
   proof
     let x be set;
     assume x in Up(W1) + Up(W2);
     then x in {u + v where u,v is Element of V:
      u in Up(W1) & v in Up(W2)} by RUSUB_4:def 10;
     then consider u,v being Element of V such that
A4:   x = u + v & u in Up(W1) & v in Up(W2);
       u in the carrier of W1 & v in the carrier of W2 by A4,RUSUB_4:def 6;
     then u in W1 & v in W2 by RLVECT_1:def 1;
     hence thesis by A1,A4;
   end;
   then Up(W1) + Up(W2) c= Up(W1+W2) by TARSKI:def 3;
   hence thesis by A3,XBOOLE_0:def 10;
end;

Lm6:
for V being RealLinearSpace, W1,W2 being Subspace of V holds
 Up(W1 /\ W2) = Up(W1) /\ Up(W2)
proof
   let V be RealLinearSpace;
   let W1,W2 be Subspace of V;
A1:Up(W1 /\ W2) = the carrier of W1 /\ W2 by RUSUB_4:def 6
    .= (the carrier of W1) /\ (the carrier of W2) by RLSUB_2:def 2;
     for x being set st x in Up(W1 /\ W2) holds x in Up(W1) /\ Up(W2)
   proof
     let x be set;
     assume x in Up(W1 /\ W2);
     then x in the carrier of W1 & x in the carrier of W2 by A1,XBOOLE_0:def 3
;
     then x in Up(W1) & x in Up(W2) by RUSUB_4:def 6;
     hence thesis by XBOOLE_0:def 3;
   end;
then A2:Up(W1 /\ W2) c= Up(W1) /\ Up(W2) by TARSKI:def 3;
     for x being set st x in Up(W1) /\ Up(W2) holds x in Up(W1 /\ W2)
   proof
     let x be set;
     assume x in Up(W1) /\ Up(W2);
     then x in Up(W1) & x in Up(W2) by XBOOLE_0:def 3;
     then x in the carrier of W1 & x in the carrier of W2 by RUSUB_4:def 6;
     hence thesis by A1,XBOOLE_0:def 3;
   end;
   then Up(W1) /\ Up(W2) c= Up(W1 /\ W2) by TARSKI:def 3;
   hence thesis by A2,XBOOLE_0:def 10;
end;

theorem Th7:
for V being RealLinearSpace, M be Subset of V holds
 Convex-Family M <> {}
proof
   let V be RealLinearSpace;
   let M be Subset of V;
A1:Up((Omega).V) is convex by CONVEX1:9;
     M c= Up((Omega).V)
   proof
       let x be set;
       assume x in M;
       then reconsider x as Element of V;
         x in the carrier of (the RLSStruct of V);
       then x in the carrier of (Omega).V by RLSUB_1:def 4;
       hence thesis by RUSUB_4:def 6;
   end;
   hence thesis by A1,CONVEX1:def 4;
end;

theorem
  for V being RealLinearSpace, M being Subset of V holds M c= conv(M)
proof
  let V be RealLinearSpace;
  let M be Subset of V;
    let v be set;
    assume
A1: v in M;
A2: Convex-Family M <> {} by Th7;
      for Y being set holds
     Y in Convex-Family M implies v in Y
    proof
      let Y be set;
      assume
A3:   Y in Convex-Family M;
      then reconsider Y as Subset of V;
        Y is convex & M c= Y by A3,CONVEX1:def 4;
      hence thesis by A1;
    end;
    then v in meet(Convex-Family M) by A2,SETFAM_1:def 1;
    hence thesis by CONVEX1:def 5;
end;

Lm7:
for V being RealLinearSpace, L1, L2 being Convex_Combination of V,
 a,b being Real st a * b > 0 holds
  Carrier(a*L1 + b*L2) = Carrier(a * L1) \/ Carrier(b * L2)
proof
   let V be RealLinearSpace;
   let L1, L2 be Convex_Combination of V;
   let a,b be Real;
   assume a * b > 0;
then A1:not (a>=0 & b<=0 or a<=0 & b>=0) by REAL_2:123;

then A2: Carrier(L1) = Carrier(a * L1) &
     Carrier(L2) = Carrier(b * L2) by RLVECT_2:65;

     for x being set st x in Carrier(a * L1) \/ Carrier(b * L2) holds
    x in Carrier(a*L1 + b*L2)
   proof
     let x be set;
     assume
A3:  x in Carrier(a * L1) \/ Carrier(b * L2);
       now per cases by A3,XBOOLE_0:def 2;
       suppose
A4:    x in Carrier(a * L1);
       then x in {v where v is Element of V : (a * L1).v <> 0}
         by RLVECT_2:def 6;
       then consider v being Element of V such that
A5:    v = x & (a * L1).v <> 0;
A6:    L1.v > 0 by A2,A4,A5,CONVEX1:22;
         v in Carrier(a*L1 + b*L2)
       proof
           now per cases;
           suppose v in Carrier(L2);
then A7:        L2.v > 0 by CONVEX1:22;

             now per cases by A1;
             suppose a > 0 & b > 0;
             then a*L1.v > 0 & b*L2.v > 0 by A6,A7,SQUARE_1:21;
then A8:          (a*L1).v > 0 & (b*L2).v > 0 by RLVECT_2:def 13;
             then (a*L1).v + (b*L2).v > (a*L1).v by REAL_1:69;
             then (a*L1).v + (b*L2).v > 0 by A8,AXIOMS:22;
             then (a*L1 + b*L2).v > 0 by RLVECT_2:def 12;
             hence thesis by RLVECT_2:28;
             suppose a < 0 & b < 0;
             then a*L1.v < 0 & b*L2.v < 0 by A6,A7,SQUARE_1:24;
then A9:          (a*L1).v < 0 & (b*L2).v < 0 by RLVECT_2:def 13;
             then (a*L1).v + (b*L2).v < (b*L2).v by REAL_2:173;
             then (a*L1).v + (b*L2).v < 0 by A9,AXIOMS:22;
             then (a*L1 + b*L2).v < 0 by RLVECT_2:def 12;
             hence thesis by RLVECT_2:28;
           end;
           hence thesis;
           suppose not v in Carrier(L2);
           then L2.v = 0 by RLVECT_2:28;
           then b*L2.v = 0;
           then (b*L2).v = 0 by RLVECT_2:def 13;
           then (a*L1).v + (b*L2).v = (a*L1).v;
           then (a*L1 + b*L2).v <> 0 by A5,RLVECT_2:def 12;
           hence thesis by RLVECT_2:28;
         end;
         hence thesis;
       end;

       hence thesis by A5;
       suppose
A10:    x in Carrier(b * L2);
       then x in {v where v is Element of V : (b * L2).v <> 0}
         by RLVECT_2:def 6;
       then consider v being Element of V such that
A11:    v = x & (b * L2).v <> 0;
A12:    L2.v > 0 by A2,A10,A11,CONVEX1:22;
         v in Carrier(a*L1 + b*L2)
       proof
           now per cases;
           suppose v in Carrier(L1);
then A13:        L1.v > 0 by CONVEX1:22;

             now per cases by A1;
             suppose a > 0 & b > 0;
             then a*L1.v > 0 & b*L2.v > 0 by A12,A13,SQUARE_1:21;
then A14:          (a*L1).v > 0 & (b*L2).v > 0 by RLVECT_2:def 13;
             then (a*L1).v + (b*L2).v > (a*L1).v by REAL_1:69;
             then (a*L1).v + (b*L2).v > 0 by A14,AXIOMS:22;
             then (a*L1 + b*L2).v > 0 by RLVECT_2:def 12;
             hence thesis by RLVECT_2:28;
             suppose a < 0 & b < 0;
             then a*L1.v < 0 & b*L2.v < 0 by A12,A13,SQUARE_1:24;
then A15:          (a*L1).v < 0 & (b*L2).v < 0 by RLVECT_2:def 13;
             then (a*L1).v + (b*L2).v < (b*L2).v by REAL_2:173;
             then (a*L1).v + (b*L2).v < 0 by A15,AXIOMS:22;
             then (a*L1 + b*L2).v < 0 by RLVECT_2:def 12;
             hence thesis by RLVECT_2:28;
           end;
           hence thesis;
           suppose not v in Carrier(L1);
           then L1.v = 0 by RLVECT_2:28;
           then a*L1.v = 0;
           then (a*L1).v = 0 by RLVECT_2:def 13;
           then (a*L1).v + (b*L2).v = (b*L2).v;
           then (a*L1 + b*L2).v <> 0 by A11,RLVECT_2:def 12;
           hence thesis by RLVECT_2:28;
         end;
         hence thesis;
       end;
       hence thesis by A11;
     end;
     hence thesis;
   end;
then A16:Carrier(a * L1) \/ Carrier(b * L2) c= Carrier(a*L1 + b*L2) by TARSKI:
def 3;
     Carrier(a*L1 + b*L2) c= Carrier(a*L1) \/ Carrier(b*L2) by RLVECT_2:58;
   hence thesis by A16,XBOOLE_0:def 10;
end;

Lm8:
for F,G being Function st F,G are_fiberwise_equipotent
 for x1,x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
  ex z1,z2 being set st
   z1 in dom G & z2 in dom G & z1 <> z2 & F.x1 = G.z1 & F.x2 = G.z2
proof
   let F,G be Function;
   assume
A1:F,G are_fiberwise_equipotent;
   let x1,x2 be set;
   assume that
A2:x1 in dom F and
A3:x2 in dom F and
A4:x1 <> x2;
   consider H being Function such that
A5:dom H = dom F & rng H = dom G & H is one-to-one & F = G*H by A1,RFINSEQ:3;
A6:H.x1 in dom G & H.x2 in dom G by A2,A3,A5,FUNCT_1:12;
A7:H.x1 <> H.x2 by A2,A3,A4,A5,FUNCT_1:def 8;
     F.x1 = G.(H.x1) & F.x2 = G.(H.x2) by A2,A3,A5,FUNCT_1:22;
   hence thesis by A6,A7;
end;

Lm9:
for V being RealLinearSpace, L being Linear_Combination of V,
 A being Subset of V st A c= Carrier(L) holds
  ex L1 being Linear_Combination of V st Carrier(L1) = A
proof
   let V be RealLinearSpace;
   let L be Linear_Combination of V;
   let A be Subset of V;
   assume
A1:A c= Carrier(L);

   consider F being Function such that
A2:L = F & dom F = the carrier of V & rng F c= REAL by FUNCT_2:def 2;

defpred P[set,set] means
 ($1 in A implies $2 = F.$1) & (not $1 in A implies $2 = 0);
A3:for x,y1,y2 being set st x in the carrier of V & P[x,y1] & P[x,y2]
  holds y1 = y2;

A4:for x being set st x in the carrier of V
    ex y being set st P[x,y]
   proof
     let x be set;
     assume x in the carrier of V;
       now per cases;
       suppose x in A;
       hence thesis;
       suppose not x in A;
       hence thesis;
     end;
     hence thesis;
   end;

   consider L1 being Function such that
A5:dom L1 = the carrier of V &
   for x being set st x in the carrier of V holds P[x,L1.x] from FuncEx(A3,A4);

     for y being set st y in rng L1 holds y in REAL
   proof
     let y be set;
     assume y in rng L1;
     then consider x being set such that
A6:  x in dom L1 & y = L1.x by FUNCT_1:def 5;
     reconsider x as Element of V by A5,A6;
       now per cases;
       suppose x in A;
then A7:    y = F.x by A5,A6;
         F.x in rng F by A2,FUNCT_1:12;
       hence thesis by A2,A7;

       suppose not x in A;
       then L1.x = 0 by A5;
       hence thesis by A6;
     end;
     hence thesis;
   end;
then rng L1 c= REAL by TARSKI:def 3;

then A8:L1 is Element of Funcs(the carrier of V, REAL)
    by A5,FUNCT_2:def 2;

   reconsider A as finite Subset of V by A1,FINSET_1:13;

     for v being Element of V st not v in A holds
    L1.v = 0 by A5;
   then reconsider L1 as Linear_Combination of V by A8,RLVECT_2:def 5;

     for v being set st v in A holds v in Carrier(L1)
   proof
     let v be set;
     assume
A9: v in A;
     then reconsider v as Element of V;
A10: L1.v = F.v by A5,A9;
       L.v <> 0 by A1,A9,RLVECT_2:28;
     hence thesis by A2,A10,RLVECT_2:28;
   end;
then A11:A c= Carrier(L1) by TARSKI:def 3;

     for v being set st v in Carrier(L1) holds v in A
   proof
     let v be set;
     assume
A12: v in Carrier(L1);
     then reconsider v as Element of V;
       L1.v <> 0 by A12,RLVECT_2:28;
     hence thesis by A5;
   end;
then A13:Carrier(L1) c= A by TARSKI:def 3;
   take L1;
   thus thesis by A11,A13,XBOOLE_0:def 10;
end;

theorem Th9:
for V being RealLinearSpace, L1,L2 being Convex_Combination of V,
 r being Real st 0 < r & r < 1 holds
  r*L1 + (1-r)*L2 is Convex_Combination of V
proof
   let V be RealLinearSpace;
   let L1,L2 be Convex_Combination of V;
   let r be Real;

   assume
A1:0 < r & r < 1;
   then r - r < 1 - r by REAL_1:54;
then A2:0 < 1 - r by XCMPLX_1:14;
then A3:r*(1-r) > 0 by A1,REAL_2:122;
   consider F1 being FinSequence of the carrier of V such that
A4:F1 is one-to-one & rng F1 = Carrier(L1) &
    (ex f being FinSequence of REAL st len f = len F1 & Sum(f) = 1 &
     (for n being Nat st n in dom f holds f.n = L1.(F1.n) & f.n >= 0))
      by CONVEX1:def 3;
   consider f1 being FinSequence of REAL such that
A5:len f1 = len F1 & Sum(f1) = 1 &
    (for n being Nat st n in dom f1 holds f1.n = L1.(F1.n) & f1.n >= 0)
     by A4;

   consider F2 being FinSequence of the carrier of V such that
A6:F2 is one-to-one & rng F2 = Carrier(L2) &
    (ex f being FinSequence of REAL st len f = len F2 & Sum(f) = 1 &
     (for n being Nat st n in dom f holds f.n = L2.(F2.n) & f.n >= 0))
      by CONVEX1:def 3;
   consider f2 being FinSequence of REAL such that
A7:len f2 = len F2 & Sum(f2) = 1 &
    (for n being Nat st n in dom f2 holds f2.n = L2.(F2.n) & f2.n >= 0)
     by A6;

   set L = r*L1 + (1-r)*L2;

A8:Carrier(r*L1) = Carrier(L1) & Carrier((1-r)*L2) = Carrier(L2)
    by A1,A2,RLVECT_2:65;
A9:Carrier(L) = Carrier(r*L1) \/ Carrier((1-r)*L2) by A3,Lm7;

   set Top = Carrier(L) \ Carrier((1-r)*L2);
   set Mid = Carrier(r*L1) /\ Carrier((1-r)*L2);
   set Btm = Carrier(L) \ Carrier(r*L1);

     Top c= Carrier(L) by XBOOLE_1:36;
   then consider Lt being Linear_Combination of V such that
A10:Carrier(Lt) = Top by Lm9;

     Mid c= Carrier(L) by A9,XBOOLE_1:29;
   then consider Lm being Linear_Combination of V such that
A11:Carrier(Lm) = Mid by Lm9;

     Btm c= Carrier(L) by XBOOLE_1:36;
   then consider Lb being Linear_Combination of V such that
A12:Carrier(Lb) = Btm by Lm9;

   consider Ft being FinSequence of the carrier of V such that
A13:Ft is one-to-one & rng Ft = Carrier(Lt) & Sum(Lt) = Sum(Lt (#) Ft)
   by RLVECT_2:def 10;

   consider Fm being FinSequence of the carrier of V such that
A14:Fm is one-to-one & rng Fm = Carrier(Lm) & Sum(Lm) = Sum(Lm (#) Fm)
   by RLVECT_2:def 10;

   consider Fb being FinSequence of the carrier of V such that
A15:Fb is one-to-one & rng Fb = Carrier(Lb) & Sum(Lb) = Sum(Lb (#) Fb)
   by RLVECT_2:def 10;
   deffunc F(set) = L1.(Ft.$1);
   consider ft being FinSequence such that
A16:len ft = len Ft &
   for j being Nat st j in Seg (len Ft) holds ft.j = F(j) from SeqLambda;

     rng ft c= REAL
   proof
       let y be set;
       assume y in rng ft;
       then consider x being set such that
A17:   x in dom ft & ft.x = y by FUNCT_1:def 5;
         Seg len ft c= NAT;
       then dom ft c= NAT by FINSEQ_1:def 3;
       then reconsider x as Nat by A17;
A18:   x in Seg len Ft by A16,A17,FINSEQ_1:def 3;
       then x in dom Ft by FINSEQ_1:def 3;
       then Ft.x in rng Ft & rng Ft c= the carrier of V
        by FINSEQ_1:def 4,FUNCT_1:12;
       then reconsider Ftx = Ft.x as Element of V;
A19:   ft.x = L1.(Ft.x) by A16,A18;
       consider L1f being Function such that
A20:   L1 = L1f & dom L1f = the carrier of V & rng L1f c= REAL
        by FUNCT_2:def 2;
         Ftx in dom L1f by A20;
       then ft.x in rng L1f by A19,A20,FUNCT_1:12;
       hence thesis by A17,A20;
   end;
   then reconsider ft as FinSequence of REAL by FINSEQ_1:def 4;

   deffunc F(set) = L1.(Fm.$1);
   consider fm1 being FinSequence such that
A21:len fm1 = len Fm &
   for j being Nat st j in Seg (len Fm) holds fm1.j = F(j) from SeqLambda;

     rng fm1 c= REAL
   proof
       let y be set;
       assume y in rng fm1;
       then consider x being set such that
A22:   x in dom fm1 & fm1.x = y by FUNCT_1:def 5;
         Seg len fm1 c= NAT;
       then dom fm1 c= NAT by FINSEQ_1:def 3;
       then reconsider x as Nat by A22;
A23:   x in Seg len Fm by A21,A22,FINSEQ_1:def 3;
       then x in dom Fm by FINSEQ_1:def 3;
       then Fm.x in rng Fm & rng Fm c= the carrier of V
        by FINSEQ_1:def 4,FUNCT_1:12;
       then reconsider Fmx = Fm.x as Element of V;
A24:   fm1.x = L1.(Fm.x) by A21,A23;
       consider L1f being Function such that
A25:   L1 = L1f & dom L1f = the carrier of V & rng L1f c= REAL
        by FUNCT_2:def 2;
         Fmx in dom L1f by A25;
       then fm1.x in rng L1f by A24,A25,FUNCT_1:12;
       hence thesis by A22,A25;
   end;
   then reconsider fm1 as FinSequence of REAL by FINSEQ_1:def 4;

   deffunc F(set) = L2.(Fm.$1);
   consider fm2 being FinSequence such that
A26:len fm2 = len Fm &
   for j being Nat st j in Seg (len Fm) holds fm2.j = F(j) from SeqLambda;

     rng fm2 c= REAL
   proof
       let y be set;
       assume y in rng fm2;
       then consider x being set such that
A27:   x in dom fm2 & fm2.x = y by FUNCT_1:def 5;
         Seg len fm2 c= NAT;
       then dom fm2 c= NAT by FINSEQ_1:def 3;
       then reconsider x as Nat by A27;
A28:   x in Seg len Fm by A26,A27,FINSEQ_1:def 3;
       then x in dom Fm by FINSEQ_1:def 3;
       then Fm.x in rng Fm & rng Fm c= the carrier of V
        by FINSEQ_1:def 4,FUNCT_1:12;
       then reconsider Fmx = Fm.x as Element of V;
A29:   fm2.x = L2.(Fm.x) by A26,A28;
       consider L2f being Function such that
A30:   L2 = L2f & dom L2f = the carrier of V & rng L2f c= REAL
        by FUNCT_2:def 2;
         Fmx in dom L2f by A30;
       then fm2.x in rng L2f by A29,A30,FUNCT_1:12;
       hence thesis by A27,A30;
   end;
   then reconsider fm2 as FinSequence of REAL by FINSEQ_1:def 4;

   deffunc F(set) = L2.(Fb.$1);
   consider fb being FinSequence such that
A31:len fb = len Fb &
   for j being Nat st j in Seg (len Fb) holds fb.j = F(j) from SeqLambda;

     rng fb c= REAL
   proof
       let y be set;
       assume y in rng fb;
       then consider x being set such that
A32:   x in dom fb & fb.x = y by FUNCT_1:def 5;
         Seg len fb c= NAT;
       then dom fb c= NAT by FINSEQ_1:def 3;
       then reconsider x as Nat by A32;
A33:   x in Seg len Fb by A31,A32,FINSEQ_1:def 3;
       then x in dom Fb by FINSEQ_1:def 3;
       then Fb.x in rng Fb & rng Fb c= the carrier of V
        by FINSEQ_1:def 4,FUNCT_1:12;
       then reconsider Fbx = Fb.x as Element of V;
A34:   fb.x = L2.(Fb.x) by A31,A33;
       consider L2f being Function such that
A35:   L2 = L2f & dom L2f = the carrier of V & rng L2f c= REAL
        by FUNCT_2:def 2;
         Fbx in dom L2f by A35;
       then fb.x in rng L2f by A34,A35,FUNCT_1:12;
       hence thesis by A32,A35;
   end;
   then reconsider fb as FinSequence of REAL by FINSEQ_1:def 4;

     Carrier(r*L1) /\ Carrier((1-r)*L2) c= Carrier((1-r)*L2) by XBOOLE_1:17;
then A36:rng Ft misses rng Fm by A10,A11,A13,A14,XBOOLE_1:85;

     Carrier(r*L1) /\ Carrier((1-r)*L2) c= Carrier(r*L1) by XBOOLE_1:17;
then A37:rng Fm misses rng Fb by A11,A12,A14,A15,XBOOLE_1:85;

A38:F1, Ft^Fm are_fiberwise_equipotent
   proof
A39: Ft^Fm is one-to-one by A13,A14,A36,FINSEQ_3:98;
       rng (Ft^Fm) = rng Ft \/ rng Fm by FINSEQ_1:44
      .= ((Carrier(L1) \/ Carrier(L2)) \ Carrier(L2))
       \/ (Carrier(L1) /\ Carrier(L2)) by A3,A8,A10,A11,A13,A14,Lm7
      .= ( Carrier(L1) \ Carrier(L2) ) \/ ( Carrier(L2) \ Carrier(L2) )
       \/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:42
      .= ( Carrier(L1) \ Carrier(L2) ) \/ {}
       \/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:37
      .= Carrier(L1) \ (Carrier(L2) \ Carrier(L2)) by XBOOLE_1:52
      .= Carrier(L1) \ {} by XBOOLE_1:37
      .= rng F1 by A4;
     hence thesis by A4,A39,VECTSP_9:4;
   end;

     f1, ft^fm1 are_fiberwise_equipotent
   proof
A40: dom L1 = the carrier of V by PRALG_3:4;
A41: for x being set holds x in dom f1 iff x in dom F1 & F1.x in dom L1
     proof
       let x be set;
A42:   now assume x in dom f1;
         then x in Seg len F1 by A5,FINSEQ_1:def 3;
         hence x in dom F1 by FINSEQ_1:def 3;
         then F1.x in rng F1 by FUNCT_1:12;
         hence F1.x in dom L1 by A4,A40;
       end;
         now assume x in dom F1 & F1.x in dom L1;
       then x in Seg len F1 by FINSEQ_1:def 3;
       hence x in dom f1 by A5,FINSEQ_1:def 3;
       end;
       hence thesis by A42;
     end;

       for x being set st x in dom f1 holds f1.x = L1.(F1.x)
     proof
       let x be set;
       assume
A43:   x in dom f1;
         Seg len f1 c= NAT;
       then dom f1 c= NAT by FINSEQ_1:def 3;
       then reconsider n = x as Nat by A43;
         f1.n = L1.(F1.n) by A5,A43;
       hence f1.x = L1.(F1.x);
     end;
then A44: f1 = L1*F1 by A41,FUNCT_1:20;
A45: rng (Ft^Fm) = Carrier(Lt) \/ Carrier(Lm) by A13,A14,FINSEQ_1:44;
A46: for x being set holds
      x in dom (ft^fm1) iff x in dom(Ft^Fm) & (Ft^Fm).x in dom L1
     proof
       let x be set;
A47:   len (ft^fm1) = len ft + len fm1 by FINSEQ_1:35
        .= len (Ft^Fm) by A16,A21,FINSEQ_1:35;

A48:   dom(ft^fm1) = Seg len(ft^fm1) by FINSEQ_1:def 3
        .= dom (Ft^Fm) by A47,FINSEQ_1:def 3;

         x in dom (ft^fm1) implies (Ft^Fm).x in dom L1
       proof
         assume x in dom (ft^fm1);
         then (Ft^Fm).x in rng (Ft^Fm) by A48,FUNCT_1:12;
then A49:     (Ft^Fm).x in Carrier(Lt) \/ Carrier(Lm) by A13,A14,FINSEQ_1:44;
           dom L1 = the carrier of V by PRALG_3:4;
         hence thesis by A49;
       end;
       hence thesis by A48;
     end;

       for x being set st x in dom(ft^fm1) holds (ft^fm1).x = L1.((Ft^Fm).x)
     proof
       let x be set;
       assume
A50:   x in dom (ft^fm1);
         Seg len (ft^fm1) c= NAT;
       then dom (ft^fm1) c= NAT by FINSEQ_1:def 3;
       then reconsider n = x as Nat by A50;
         now per cases by A50,FINSEQ_1:38;
         suppose
A51:     n in dom ft;
then A52:     n in Seg len Ft by A16,FINSEQ_1:def 3;
         then ft.n = L1.(Ft.n) by A16;
then A53:     (ft^fm1).n = L1.(Ft.n) by A51,FINSEQ_1:def 7;
           n in dom Ft by A52,FINSEQ_1:def 3;
         hence thesis by A53,FINSEQ_1:def 7;

         suppose ex m being Nat st m in dom fm1 & n = len ft + m;
         then consider m being Nat such that
A54:     m in dom fm1 & n = len ft + m;
A55:     m in Seg len Fm by A21,A54,FINSEQ_1:def 3;
A56:     (ft^fm1).n = fm1.m by A54,FINSEQ_1:def 7
          .= L1.(Fm.m) by A21,A55;
           m in dom Fm & n = len Ft + m by A16,A54,A55,FINSEQ_1:def 3;
         hence thesis by A56,FINSEQ_1:def 7;
       end;
       hence thesis;
     end;
then A57: (ft^fm1) = L1*(Ft^Fm) by A46,FUNCT_1:20;
       dom F1 = dom (Ft^Fm) by A38,RFINSEQ:16;
     hence thesis by A4,A38,A40,A44,A45,A57,BAGORDER:4;
   end;
then A58:Sum(f1) = Sum(ft^fm1) by RFINSEQ:22;
A59:F2, Fm^Fb are_fiberwise_equipotent
   proof
A60: Fm^Fb is one-to-one by A14,A15,A37,FINSEQ_3:98;
       rng (Fm^Fb) = (Carrier(L) \ Carrier(r*L1))
       \/ (Carrier(r*L1) /\ Carrier((1-r)*L2)) by A11,A12,A14,A15,FINSEQ_1:44
      .= ((Carrier(L1) \/ Carrier(L2)) \ Carrier(L1))
       \/ (Carrier(L1) /\ Carrier(L2)) by A3,A8,Lm7
      .= ( Carrier(L1) \ Carrier(L1) ) \/ ( Carrier(L2) \ Carrier(L1) )
       \/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:42
      .= ( Carrier(L2) \ Carrier(L1) ) \/ {}
       \/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:37
      .= Carrier(L2) \ (Carrier(L1) \ Carrier(L1)) by XBOOLE_1:52
      .= Carrier(L2) \ {} by XBOOLE_1:37
      .= rng F2 by A6;
     hence thesis by A6,A60,VECTSP_9:4;
   end;

     f2, fm2^fb are_fiberwise_equipotent
   proof
A61: dom L2 = the carrier of V by PRALG_3:4;

A62: for x being set holds x in dom f2 iff x in dom F2 & F2.x in dom L2
     proof
       let x be set;
A63:   now assume
           x in dom f2;
         then x in Seg len F2 by A7,FINSEQ_1:def 3;
         hence x in dom F2 by FINSEQ_1:def 3;
         then F2.x in rng F2 by FUNCT_1:12;
         hence F2.x in dom L2 by A6,A61;
       end;
         now assume x in dom F2 & F2.x in dom L2;
       then x in Seg len F2 by FINSEQ_1:def 3;
       hence x in dom f2 by A7,FINSEQ_1:def 3;
       end;
       hence thesis by A63;
     end;

       for x being set st x in dom f2 holds f2.x = L2.(F2.x)
     proof
       let x be set;
       assume
A64:   x in dom f2;
         Seg len f2 c= NAT;
       then dom f2 c= NAT by FINSEQ_1:def 3;
       then reconsider n = x as Nat by A64;
         f2.n = L2.(F2.n) by A7,A64;
       hence f2.x = L2.(F2.x);
     end;
then A65: f2 = L2*F2 by A62,FUNCT_1:20;

A66: rng (Fm^Fb) = Carrier(Lm) \/ Carrier(Lb) by A14,A15,FINSEQ_1:44;

A67: for x being set holds
      x in dom (fm2^fb) iff x in dom(Fm^Fb) & (Fm^Fb).x in dom L2
     proof
       let x be set;
A68:   len (fm2^fb) = len fm2 + len fb by FINSEQ_1:35
        .= len (Fm^Fb) by A26,A31,FINSEQ_1:35;

A69:   dom(fm2^fb) = Seg len(fm2^fb) by FINSEQ_1:def 3
        .= dom (Fm^Fb) by A68,FINSEQ_1:def 3;

         x in dom (fm2^fb) implies (Fm^Fb).x in dom L2
       proof
         assume x in dom (fm2^fb);
         then (Fm^Fb).x in rng (Fm^Fb) by A69,FUNCT_1:12;
then A70:     (Fm^Fb).x in Carrier(Lm) \/ Carrier(Lb) by A14,A15,FINSEQ_1:44;
           dom L2 = the carrier of V by PRALG_3:4;
         hence thesis by A70;
       end;
       hence thesis by A69;
     end;

       for x being set st x in dom(fm2^fb) holds (fm2^fb).x = L2.((Fm^Fb).x)
     proof
       let x be set;
       assume
A71:   x in dom (fm2^fb);
         Seg len (fm2^fb) c= NAT;
       then dom (fm2^fb) c= NAT by FINSEQ_1:def 3;
       then reconsider n = x as Nat by A71;
         now per cases by A71,FINSEQ_1:38;
         suppose
A72:     n in dom fm2;
then A73:     n in Seg len Fm by A26,FINSEQ_1:def 3;
         then fm2.n = L2.(Fm.n) by A26;
then A74:     (fm2^fb).n = L2.(Fm.n) by A72,FINSEQ_1:def 7;
           n in dom Fm by A73,FINSEQ_1:def 3;
         hence thesis by A74,FINSEQ_1:def 7;

         suppose ex m being Nat st m in dom fb & n = len fm2 + m;
         then consider m being Nat such that
A75:     m in dom fb & n = len fm2 + m;
A76:     m in Seg len Fb by A31,A75,FINSEQ_1:def 3;
A77:     (fm2^fb).n = fb.m by A75,FINSEQ_1:def 7
          .= L2.(Fb.m) by A31,A76;
           m in dom Fb & n = len Fm + m by A26,A75,A76,FINSEQ_1:def 3;
         hence thesis by A77,FINSEQ_1:def 7;
       end;
       hence thesis;
     end;
then A78: (fm2^fb) = L2*(Fm^Fb) by A67,FUNCT_1:20;
       dom F2 = dom (Fm^Fb) by A59,RFINSEQ:16;
     hence thesis by A6,A59,A61,A65,A66,A78,BAGORDER:4;
   end;
then A79:Sum(f2) = Sum(fm2^fb) by RFINSEQ:22;

   set F = Ft^Fm^Fb;
   set f = (r*ft)^(r*fm1 + (1-r)*fm2)^((1-r)*fb);

A80:rng (Ft^Fm) = Carrier(L1) by A4,A38,RFINSEQ:1;
A81:rng Fb = Carrier(L) \ Carrier(L1) by A1,A12,A15,RLVECT_2:65;
then A82:rng (Ft^Fm) misses rng Fb by A80,XBOOLE_1:79;
     Ft^Fm is one-to-one by A13,A14,A36,FINSEQ_3:98;
then A83:F is one-to-one by A15,A82,FINSEQ_3:98;
A84:Carrier(L1) c= Carrier(L) by A8,A9,XBOOLE_1:7;
A85:rng F = Carrier(L1) \/ (Carrier(L) \ Carrier(L1)) by A80,A81,FINSEQ_1:44
    .= Carrier(L1) \/ Carrier(L) by XBOOLE_1:39
    .= Carrier(L) by A84,XBOOLE_1:12;

     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
   proof
A86: len (r*fm1) = len fm1 by EUCLID_2:8
      .= len ((1-r)*fm2) by A21,A26,EUCLID_2:8;

       len f = len ((r*ft)^(r*fm1 + (1-r)*fm2)) + len((1-r)*fb) by FINSEQ_1:35
      .= len(r*ft) + len(r*fm1 + (1-r)*fm2) + len((1-r)*fb) by FINSEQ_1:35
      .= len ft + len(r*fm1 + (1-r)*fm2) + len((1-r)*fb) by EUCLID_2:8
      .= len ft + len(r*fm1 + (1-r)*fm2) + len fb by EUCLID_2:8
      .= len ft + len (r*fm1) + len fb by A86,INTEGRA5:2
      .= len Ft + len Fm + len Fb by A16,A21,A31,EUCLID_2:8
      .= len (Ft^Fm) + len Fb by FINSEQ_1:35;
     hence len f = len F by FINSEQ_1:35;

       Sum(f) = Sum((r*ft)^(r*fm1 + (1-r)*fm2)) + Sum((1-r)*fb) by RVSUM_1:105
      .= Sum(r*ft) + Sum(r*fm1 + (1-r)*fm2) + Sum((1-r)*fb) by RVSUM_1:105
      .= r*Sum(ft) + Sum(r*fm1 + (1-r)*fm2) + Sum((1-r)*fb) by RVSUM_1:117
      .= r*Sum(ft) + Sum(r*fm1 + (1-r)*fm2) + (1-r)*Sum(fb) by RVSUM_1:117
      .= r*Sum(ft) + ( Sum(r*fm1) + Sum((1-r)*fm2) ) + (1-r)*Sum(fb)
          by A86,INTEGRA5:2
      .= r*Sum(ft)+( r*Sum(fm1) + Sum((1-r)*fm2) )+(1-r)*Sum(fb) by RVSUM_1:117
      .= r*Sum(ft)+( r*Sum(fm1) + (1-r)*Sum(fm2) )+(1-r)*Sum(fb) by RVSUM_1:117
      .= r*Sum(ft)+ r*Sum(fm1) + (1-r)*Sum(fm2) +(1-r)*Sum(fb) by XCMPLX_1:1
      .= r*(Sum(ft)+Sum(fm1)) + (1-r)*Sum(fm2) +(1-r)*Sum(fb) by XCMPLX_1:8
      .= r*(Sum(ft)+Sum(fm1)) + ((1-r)*Sum(fm2) +(1-r)*Sum(fb)) by XCMPLX_1:1
      .= r*(Sum(ft)+Sum(fm1)) + (1-r)*(Sum(fm2)+Sum(fb)) by XCMPLX_1:8
      .= r*(Sum(ft^fm1)) + (1-r)*(Sum(fm2)+Sum(fb)) by RVSUM_1:105
      .= r*1 + (1-r)*1 by A5,A7,A58,A79,RVSUM_1:105
      .= r + 1 - r by XCMPLX_1:29
      .= r - r + 1 by XCMPLX_1:29
      .= 0 + 1 by XCMPLX_1:14;
     hence Sum(f) = 1;
       for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
     proof
       let n be Nat;
       assume
A87:   n in dom f;
         now per cases by A87,FINSEQ_1:38;
         suppose
A88:     n in dom ((r*ft)^(r*fm1 + (1-r)*fm2));
then A89:     f.n = ((r*ft)^(r*fm1 + (1-r)*fm2)).n by FINSEQ_1:def 7;
           now per cases by A88,FINSEQ_1:38;
           suppose
A90:       n in dom(r*ft);
           then n in dom ft by RVSUM_1:65;
then A91:       n in Seg len Ft by A16,FINSEQ_1:def 3;
A92:       f.n = (r*ft).n by A89,A90,FINSEQ_1:def 7
              .= r*(ft.n) by RVSUM_1:66
              .= r*(L1.(Ft.n)) by A16,A91;
A93:        n in dom Ft by A91,FINSEQ_1:def 3;
then A94:        Ft.n in rng Ft by FUNCT_1:12;
A95:        Ft.n in Carrier(Lt) by A13,A93,FUNCT_1:12;
           then reconsider Ftn = Ft.n as Element of V;
             Ft.n in Carrier(L) & not Ft.n in Carrier(L2)
             by A8,A10,A95,XBOOLE_0:def 4;
           then L2.(Ftn) = 0 by RLVECT_2:28;
           then (1-r)*L2.(Ftn) = 0;
           then ((1-r)*L2).(Ftn) = 0 by RLVECT_2:def 13;
then A96:        f.n = (r*L1).(Ftn) + ((1-r)*L2).(Ftn) by A92,RLVECT_2:def 13
            .= (r*L1 + (1-r)*L2).(Ft.n) by RLVECT_2:def 12;

             len((r*ft)^(r*fm1+(1-r)*fm2))
             = len(r*ft) + len(r*fm1 + (1-r)*fm2) by FINSEQ_1:35
            .= len ft + len(r*fm1 + (1-r)*fm2) by EUCLID_2:8
            .= len ft + len (r*fm1) by A86,INTEGRA5:2
            .= len Ft + len Fm by A16,A21,EUCLID_2:8
            .= len (Ft^Fm) by FINSEQ_1:35;
           then n in Seg len(Ft^Fm) by A88,FINSEQ_1:def 3;
           then n in dom (Ft^Fm) by FINSEQ_1:def 3;
           then (Ft^Fm).n = F.n by FINSEQ_1:def 7;
           hence f.n = L.(F.n) by A93,A96,FINSEQ_1:def 7;

             rng Ft c= rng (Ft^Fm) by FINSEQ_1:42;
           then Ft.n in rng (Ft^Fm) by A94;
           then Ft.n in rng F1 by A38,RFINSEQ:1;
           then consider m' being set such that
A97:       m' in dom F1 & F1.m' = Ft.n by FUNCT_1:def 5;
             Seg len F1 c= NAT;
           then dom F1 c= NAT by FINSEQ_1:def 3;
           then reconsider m' as Nat by A97;
             m' in Seg len f1 by A5,A97,FINSEQ_1:def 3;
           then m' in dom f1 by FINSEQ_1:def 3;
           then f1.m' = L1.(F1.m') & f1.m' >= 0 by A5;
           hence f.n >= 0 by A1,A92,A97,SQUARE_1:19;

           suppose
             ex k being Nat st k in dom(r*fm1 + (1-r)*fm2) &
            n = len(r*ft) + k;
           then consider m being Nat such that
A98:        m in dom(r*fm1 + (1-r)*fm2) & n=len(r*ft)+m;
             len (r*fm1) = len fm1 by EUCLID_2:8
            .= len ((1-r)*fm2) by A21,A26,EUCLID_2:8;
           then len (r*fm1 + (1-r)*fm2) = len (r*fm1) by INTEGRA5:2
            .= len fm1 by EUCLID_2:8;
then A99:        m in Seg len Fm by A21,A98,FINSEQ_1:def 3;

A100:        f.n = (r*fm1 + (1-r)*fm2).m by A89,A98,FINSEQ_1:def 7
              .= (r*fm1).m + ((1-r)*fm2).m by A98,RVSUM_1:26
              .= r*(fm1.m) + ((1-r)*fm2).m by RVSUM_1:66
              .= r*(fm1.m) + (1-r)*(fm2.m) by RVSUM_1:66
              .= r*(L1.(Fm.m)) + (1-r)*(fm2.m) by A21,A99
              .= r*(L1.(Fm.m)) + (1-r)*(L2.(Fm.m)) by A26,A99;

A101:        m in dom Fm by A99,FINSEQ_1:def 3;
then A102:        Fm.m in rng Fm by FUNCT_1:12;
           then reconsider Fmm = Fm.m as Element of V by A14;
         r*(L1.(Fmm)) = (r*L1).(Fm.m) &
           (1-r)*(L2.(Fmm)) = ((1-r)*L2).(Fm.m) by RLVECT_2:def 13;
then A103:        f.n = (r*L1 + (1-r)*L2).(Fm.m) by A100,RLVECT_2:def 12;

             len((r*ft)^(r*fm1+(1-r)*fm2))
             = len(r*ft) + len(r*fm1 + (1-r)*fm2) by FINSEQ_1:35
            .= len ft + len(r*fm1 + (1-r)*fm2) by EUCLID_2:8
            .= len ft + len (r*fm1) by A86,INTEGRA5:2
            .= len Ft + len Fm by A16,A21,EUCLID_2:8
            .= len (Ft^Fm) by FINSEQ_1:35;
           then n in Seg len(Ft^Fm) by A88,FINSEQ_1:def 3;
           then n in dom (Ft^Fm) by FINSEQ_1:def 3;
then A104:        (Ft^Fm).n = F.n by FINSEQ_1:def 7;

             len(r*ft) = len Ft by A16,EUCLID_2:8;
           hence f.n = L.(F.n) by A98,A101,A103,A104,FINSEQ_1:def 7;

             rng Fm c= rng (Ft^Fm) by FINSEQ_1:43;
           then Fm.m in rng (Ft^Fm) by A102;
           then Fm.m in rng F1 by A38,RFINSEQ:1;
           then consider m' being set such that
A105:       m' in dom F1 & F1.m' = Fm.m by FUNCT_1:def 5;
             Seg len F1 c= NAT;
           then dom F1 c= NAT by FINSEQ_1:def 3;
           then reconsider m' as Nat by A105;
             m' in Seg len F1 by A105,FINSEQ_1:def 3;
           then m' in dom f1 by A5,FINSEQ_1:def 3;
           then f1.m' = L1.(F1.m') & f1.m' >= 0 by A5;
then A106:        r*L1.(Fm.m) >= 0 by A1,A105,SQUARE_1:19;

             rng Fm c= rng (Fm^Fb) by FINSEQ_1:42;
           then Fm.m in rng (Fm^Fb) by A102;
           then Fm.m in rng F2 by A59,RFINSEQ:1;
           then consider m' being set such that
A107:       m' in dom F2 & F2.m' = Fm.m by FUNCT_1:def 5;
             Seg len F2 c= NAT;
           then dom F2 c= NAT by FINSEQ_1:def 3;
           then reconsider m' as Nat by A107;
             m' in Seg len F2 by A107,FINSEQ_1:def 3;
           then m' in dom f2 by A7,FINSEQ_1:def 3;
           then f2.m' = L2.(F2.m') & f2.m' >= 0 by A7;
           then (1-r)*L2.(Fm.m) >= 0 by A2,A107,SQUARE_1:19;
           then r*(L1.(Fm.m)) + (1-r)*(L2.(Fm.m)) >= 0 + 0 by A106,REAL_1:55;
           hence f.n >= 0 by A100;
         end;
         hence thesis;

         suppose ex m being Nat st m in dom((1-r)*fb) &
         n = len ((r*ft)^(r*fm1 + (1-r)*fm2)) + m;
         then consider m being Nat such that
A108:      m in dom((1-r)*fb) & n=len((r*ft)^(r*fm1+(1-r)*fm2))+m;
           m in dom fb by A108,RVSUM_1:65;
then A109:      m in Seg len Fb by A31,FINSEQ_1:def 3;
A110:      f.n = ((1-r)*fb).m by A108,FINSEQ_1:def 7
          .= (1-r)*(fb.m) by RVSUM_1:66
          .= (1-r)*(L2.(Fb.m)) by A31,A109;

A111:      m in dom Fb by A109,FINSEQ_1:def 3;
then A112:      Fb.m in rng Fb by FUNCT_1:12;
         then reconsider Fbm = Fb.m as Element of V by A15;

           Fb.m in Carrier(L) & not Fb.m in Carrier(L1)
           by A8,A12,A15,A112,XBOOLE_0:def 4;
         then L1.(Fbm) = 0 by RLVECT_2:28;
         then r*L1.(Fbm) = 0;
         then (r*L1).(Fbm) = 0 by RLVECT_2:def 13;
then A113:      f.n = (r*L1).(Fbm) + ((1-r)*L2).(Fbm) by A110,RLVECT_2:def 13
            .= (r*L1 + (1-r)*L2).(Fb.m) by RLVECT_2:def 12;

           len((r*ft)^(r*fm1+(1-r)*fm2))
           = len(r*ft) + len(r*fm1 + (1-r)*fm2) by FINSEQ_1:35
          .= len ft + len(r*fm1 + (1-r)*fm2) by EUCLID_2:8
          .= len ft + len (r*fm1) by A86,INTEGRA5:2
          .= len Ft + len Fm by A16,A21,EUCLID_2:8
          .= len (Ft^Fm) by FINSEQ_1:35;
         hence f.n = L.(F.n) by A108,A111,A113,FINSEQ_1:def 7;

           rng Fb c= rng (Fm^Fb) by FINSEQ_1:43;
         then Fb.m in rng (Fm^Fb) by A112;
         then Fb.m in rng F2 by A59,RFINSEQ:1;
         then consider m' being set such that
A114:     m' in dom F2 & F2.m' = Fb.m by FUNCT_1:def 5;
           Seg len F2 c= NAT;
         then dom F2 c= NAT by FINSEQ_1:def 3;
         then reconsider m' as Nat by A114;
           m' in Seg len F2 by A114,FINSEQ_1:def 3;
         then m' in dom f2 by A7,FINSEQ_1:def 3;
         then f2.m' = L2.(F2.m') & f2.m' >= 0 by A7;
         hence f.n >= 0 by A2,A110,A114,SQUARE_1:19;
       end;
       hence thesis;
     end;
     hence thesis;
   end;
   hence thesis by A83,A85,CONVEX1:def 3;
end;

theorem
  for V being RealLinearSpace, M being non empty Subset of V,
 L1,L2 being Convex_Combination of M,
 r being Real st 0 < r & r < 1 holds
  r*L1 + (1-r)*L2 is Convex_Combination of M
proof
   let V be RealLinearSpace;
   let M be non empty Subset of V;
   let L1,L2 be Convex_Combination of M;
   let r be Real;
   assume
A1:0 < r & r < 1;
A2:r*L1 is Linear_Combination of M by RLVECT_2:67;
     (1-r)*L2 is Linear_Combination of M by RLVECT_2:67;
   hence thesis by A1,A2,Th9,RLVECT_2:59;
end;

theorem
  for V being RealLinearSpace holds
 ex L being Linear_Combination of V st L is convex by Lm3;

theorem
  for V being RealLinearSpace, M being non empty Subset of V holds
 ex L being Linear_Combination of M st L is convex by Lm4;

begin  :: Miscellaneous

theorem
  for V being RealLinearSpace, W1,W2 being Subspace of V holds
 Up(W1+W2) = Up(W1) + Up(W2) by Lm5;

theorem
  for V being RealLinearSpace, W1,W2 being Subspace of V holds
 Up(W1 /\ W2) = Up(W1) /\ Up(W2) by Lm6;

theorem
  for V being RealLinearSpace, L1, L2 being Convex_Combination of V,
 a,b being Real st a * b > 0 holds
  Carrier(a*L1 + b*L2) = Carrier(a * L1) \/ Carrier(b * L2) by Lm7;

theorem
  for F,G being Function st F,G are_fiberwise_equipotent
 for x1,x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
  ex z1,z2 being set st
   z1 in dom G & z2 in dom G & z1 <> z2 & F.x1 = G.z1 & F.x2 = G.z2 by Lm8;

theorem
  for V being RealLinearSpace, L being Linear_Combination of V,
 A being Subset of V st A c= Carrier(L) holds
  ex L1 being Linear_Combination of V st Carrier(L1) = A by Lm9;

Back to top