let V be RealLinearSpace; :: thesis:
let M be non empty Subset of V; :: thesis:
let L be Convex_Combination of M; :: thesis:
consider F being FinSequence of the carrier of V such that
A1: F is one-to-one and
A2: rng F = Carrier L and
A3: 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 CONVEX1:def 3;
A4: for n, m being Nat st 1 <= n & n < m & m <= len F holds
F . n <> F . m

proof

let n, m be Nat; :: thesis:
assume that
A5: 1 <= n and
A6: n < m and
A7: m <= len F ; :: thesis:
n <= len F by A6, A7, XXREAL_0:2;
then n in Seg (len F) by A5, FINSEQ_1:1;
then A8: n in dom F by FINSEQ_1:def 3;
1 <= m by A5, A6, XXREAL_0:2;
then m in Seg (len F) by A7, FINSEQ_1:1;
then A9: m in dom F by FINSEQ_1:def 3;
assume F . n = F . m ; :: thesis:
hence contradiction by A1, A6, A8, A9, FUNCT_1:def 4; :: thesis:

end;

assume A10: card (Carrier L) >= 2 ; :: thesis:
then A11: len F >= 2 by A2, A4, GRAPH_5:7;
then consider i being Nat such that
A12: len F = i + 1 by NAT_1:6;
set v = F . (len F);
A13: Carrier L c= M by RLVECT_2:def 6;
1 <= len F by A11, XXREAL_0:2;
then A14: len F in dom F by FINSEQ_3:25;
then A15: F . (len F) in rng F by FUNCT_1:3;
rng F c= the carrier of V by FINSEQ_1:def 4;
then reconsider v = F . (len F) as VECTOR of V by A15;
A16: F . (len F) in rng F by A14, FUNCT_1:3;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
consider f being FinSequence of REAL such that
A17: len f = len F and
A18: Sum f = 1 and
A19: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A3;
1 <= len f by A17, A11, XXREAL_0:2;
then A20: 1 in Seg (len f) by FINSEQ_1:1;
then A21: 1 in dom f by FINSEQ_1:def 3;
1 in dom F by A17, A20, FINSEQ_1:def 3;
then F . 1 in rng F by FUNCT_1:3;
then A22: L . (F . 1) <> 0 by A2, RLVECT_2:19;
A23: for k being Nat st k in dom (f | i) holds
0 <= (f | i) . k

proof

end;

len F >= 1 + 1 by A10, A2, A4, GRAPH_5:7;
then (len F) - 1 >= 1 by XREAL_1:19;
then 1 in Seg i by A12, FINSEQ_1:1;
then A26: 1 in dom (f | (Seg i)) by A21, RELAT_1:57;
f | i = f | (Seg i) by FINSEQ_1:def 16;
then A27: (f | i) . 1 = f . 1 by A26, FUNCT_1:47
.= L . (F . 1) by A19, A21 ;
A28: 1 in dom (f | i) by A26, FINSEQ_1:def 16;
then (f | i) . 1 >= 0 by A23;
then A29: Sum (f | i) > 0 by A23, A28, A27, A22, RVSUM_1:85;
1 <= len f by A17, A11, XXREAL_0:2;
then len f in Seg (len f) by FINSEQ_1:1;
then A30: len f in dom f by FINSEQ_1:def 3;
reconsider r = f . (len f) as Real ;
A31: f = (f | i) ^ (f /^ i) by RFINSEQ:8;
for n, m being Element of NAT st n in dom (F | i) & m in dom (F | i) & (F | i) /. n = (F | i) /. m holds
n = m

proof

A32: dom (F | i) c= dom F by FINSEQ_5:18;
let n, m be Element of NAT ; :: thesis:
assume that
A33: n in dom (F | i) and
A34: m in dom (F | i) and
A35: (F | i) /. n = (F | i) /. m ; :: thesis:
F /. n = (F | i) /. n by A33, FINSEQ_4:70
.= F /. m by A34, A35, FINSEQ_4:70 ;
hence n = m by A1, A33, A34, A32, PARTFUN2:10; :: thesis:

end;

then A36: F | i is one-to-one by PARTFUN2:9;
reconsider B = {v} as non empty Subset of V ;
consider L1 being Convex_Combination of V such that
Sum L1 = v and
A37: for A being non empty Subset of V st v in A holds
L1 is Convex_Combination of A by Th1;
A38: f = (f | i) ^ (f /^ i) by RFINSEQ:8;
set r9 = 1 / (1 - r);
defpred S₁[ object , object ] means ( ( $1 in (rng F) \ {v} implies $2 = (1 / (1 - r)) * (L . $1) ) & ( not $1 in (rng F) \ {v} implies $2 = 0 ) );
A39: for x being object st x in the carrier of V holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis:
assume x in the carrier of V ; :: thesis:
( x in (rng F) \ {v} or not x in (rng F) \ {v} ) ;
hence ex y being object st S₁[x,y] ; :: thesis:

end;

consider L2 being Function such that
A40: ( dom L2 = the carrier of V & ( for x being object st x in the carrier of V holds
S₁[x,L2 . x] ) ) from CLASSES1:sch 1(A39);
for y being object st y in rng L2 holds
y in REAL

proof

let y be object ; :: thesis:
assume y in rng L2 ; :: thesis:
then consider x being object such that
A41: x in dom L2 and
A42: y = L2 . x by FUNCT_1:def 3;

per cases ;

suppose A43: x in (rng F) \ {v} ; :: thesis:

then x in rng F ;
then reconsider x = x as VECTOR of V by A2;
y = (1 / (1 - r)) * (L . x) by A40, A42, A43
.= ((1 / (1 - r)) * L) . x by RLVECT_2:def 11 ;
hence y in REAL ; :: thesis:

end;

suppose not x in (rng F) \ {v} ; :: thesis:

then y = In (0,REAL) by A40, A41, A42;
hence y in REAL ; :: thesis:

end;

then rng L2 c= REAL ;
then A44: L2 is Element of Funcs ( the carrier of V,REAL) by A40, FUNCT_2:def 2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds
L2 . v = 0

proof

reconsider T = (Carrier L) \ {v} as finite Subset of V ;
take T ; :: thesis:
thus for v being Element of V st not v in T holds
L2 . v = 0 by A2, A40; :: thesis:

end;

then reconsider L2 = L2 as Linear_Combination of V by A44, RLVECT_2:def 3;
for u being object st u in Carrier L2 holds
u in (Carrier L) \ {v}

proof

let u be object ; :: thesis:
assume A45: u in Carrier L2 ; :: thesis:
then reconsider u = u as Element of V ;
L2 . u <> 0 by A45, RLVECT_2:19;
hence u in (Carrier L) \ {v} by A2, A40; :: thesis:

end;

then A46: Carrier L2 c= (Carrier L) \ {v} ;
f /^ i = <*(f . (len f))*> by A17, A12, FINSEQ_5:30;
then A47: Sum f = (Sum (f | i)) + r by A31, RVSUM_1:74;
then Sum (f | i) = 1 - r by A18;
then A48: 1 > r + 0 by A29, XREAL_1:20;
A49: 1 / (1 - r) > 0 by A18, A47, A29, XREAL_1:139;
for u being object st u in (Carrier L) \ {v} holds
u in Carrier L2

proof

let u be object ; :: thesis:
assume A50: u in (Carrier L) \ {v} ; :: thesis:
then reconsider u = u as Element of V ;
u in Carrier L by A50, XBOOLE_0:def 5;
then A51: L . u <> 0 by RLVECT_2:19;
L2 . u = (1 / (1 - r)) * (L . u) by A2, A40, A50;
then L2 . u <> 0 by A49, A51, XCMPLX_1:6;
hence u in Carrier L2 by RLVECT_2:19; :: thesis:

end;

then (Carrier L) \ {v} c= Carrier L2 ;
then A52: Carrier L2 = (Carrier L) \ {v} by A46, XBOOLE_0:def 10;
then Carrier L2 c= Carrier L by XBOOLE_1:36;
then Carrier L2 c= M by A13;
then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def 6;
deffunc H₁( set ) -> set = L2 . ((F | i) . $1);
consider f2 being FinSequence such that
A53: ( len f2 = len (F | i) & ( for k being Nat st k in dom f2 holds
f2 . k = H₁(k) ) ) from FINSEQ_1:sch 2();
F = (F | i) ^ (F /^ i) by RFINSEQ:8;
then Carrier L = (rng (F | i)) \/ (rng (F /^ i)) by A2, FINSEQ_1:31;
then A54: (Carrier L) \ (rng (F /^ i)) = rng (F | i) by A1, FINSEQ_5:34, XBOOLE_1:88;
for y being object st y in rng f2 holds
y in REAL

proof

let y be object ; :: thesis:
A55: ex L29 being Function st
( L2 = L29 & dom L29 = the carrier of V & rng L29 c= REAL ) by FUNCT_2:def 2;
assume y in rng f2 ; :: thesis:
then consider x being object such that
A56: x in dom f2 and
A57: y = f2 . x by FUNCT_1:def 3;
A58: x in Seg (len f2) by A56, FINSEQ_1:def 3;
reconsider x = x as Element of NAT by A56;
x in dom (F | i) by A53, A58, FINSEQ_1:def 3;
then (F | i) . x in rng (F | i) by FUNCT_1:3;
then L2 . ((F | i) . x) in rng L2 by A54, A55, FUNCT_1:3;
then L2 . ((F | i) . x) in REAL ;
hence y in REAL by A53, A56, A57; :: thesis:

end;

then rng f2 c= REAL ;
then reconsider f2 = f2 as FinSequence of REAL by FINSEQ_1:def 4;
A59: dom f2 = Seg (len (F | i)) by A53, FINSEQ_1:def 3;
then A60: dom f2 = Seg i by A12, FINSEQ_1:59, NAT_1:12
.= Seg (len (f | i)) by A17, A12, FINSEQ_1:59, NAT_1:12
.= dom (f | i) by FINSEQ_1:def 3 ;
A61: (len F) - 1 = i by A12;
A62: for k being Element of NAT st k in dom f2 holds
( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 )

proof

let k be Element of NAT ; :: thesis:
assume A63: k in dom f2 ; :: thesis:
then A64: f2 . k = L2 . ((F | i) . k) by A53;
k in dom (f | (Seg i)) by A60, A63, FINSEQ_1:def 16;
then k in (dom f) /\ (Seg i) by RELAT_1:61;
then A65: k in dom f by XBOOLE_0:def 4;
A66: k in dom (F | i) by A59, A63, FINSEQ_1:def 3;
then (F | i) . k in rng (F | i) by FUNCT_1:3;
then reconsider w = (F | i) . k as Element of V by A54;
A67: F | i = F | (Seg i) by FINSEQ_1:def 16;
then A68: (F | i) . k = F . k by A66, FUNCT_1:47;
A69: not w in {v}

proof

( k <= len (F | i) & len (F | i) <= i ) by A59, A63, FINSEQ_1:1, FINSEQ_5:17;
then k <= i by XXREAL_0:2;
then A70: k + 1 <= len F by A61, XREAL_1:19;
assume w in {v} ; :: thesis:
then A71: F . k = v by A68, TARSKI:def 1;
dom (F | (Seg i)) c= dom F by RELAT_1:60;
then k = len F by A1, A14, A66, A67, A71, FUNCT_1:def 4;
hence contradiction by A70, NAT_1:13; :: thesis:

end;

per cases ;

suppose A75: w in (rng F) \ {v} ; :: thesis:

f . k >= 0 by A19, A65;
then A76: (1 / (1 - r)) * ((f | i) . k) >= 0 by A18, A47, A29, A72;
L2 . w = (1 / (1 - r)) * (L . w) by A40, A75
.= (1 / (1 - r)) * ((f | i) . k) by A73, A66, A67, FUNCT_1:47
.= ((1 / (1 - r)) * (f | i)) . k by RVSUM_1:44 ;
hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A64, A76, RVSUM_1:44; :: thesis:

end;

suppose A77: not w in (rng F) \ {v} ; :: thesis:

then not w in rng F by A69, XBOOLE_0:def 5;
then L . w = 0 by A2, RLVECT_2:19;
then A78: (1 / (1 - r)) * ((f | i) . k) = 0 by A74;
f2 . k = 0 by A40, A64, A77;
hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A78, RVSUM_1:44; :: thesis:

end;

then A79: for n being Nat st n in dom f2 holds
( f2 . n = L2 . ((F | i) . n) & f2 . n >= 0 ) by A53;
f /^ i = <*(f . (len f))*> by A17, A12, FINSEQ_5:30;
then A80: Sum f = (Sum (f | i)) + r by A38, RVSUM_1:74;
F /^ i = <*(F . (len F))*> by A12, FINSEQ_5:30;
then A81: rng (F | i) = Carrier L2 by A52, A54, FINSEQ_1:38;
A82: for k being Nat st k in dom f2 holds
f2 . k = ((1 / (1 - r)) * (f | i)) . k by A62;
dom f2 = dom ((1 / (1 - r)) * (f | i)) by A60, VALUED_1:def 5;
then f2 = (1 / (1 - r)) * (f | i) by A82, FINSEQ_1:13;
then Sum f2 = (1 / (1 - r)) * (1 - r) by A18, A80, RVSUM_1:87
.= 1 / ((1 - r) / (1 - r)) by XCMPLX_1:81
.= 1 / 1 by A18, A47, A29, XCMPLX_1:60
.= 1 ;
then reconsider L2 = L2 as Convex_Combination of M by A36, A81, A53, A79, CONVEX1:def 3;
A83: v in Carrier L by A2, A14, FUNCT_1:3;
then {v} c= Carrier L by ZFMISC_1:31;
then A84: card (Carrier L2) = (card (Carrier L)) - (card {v}) by A52, CARD_2:44;
Carrier L c= M by RLVECT_2:def 6;
then reconsider L1 = L1 as Convex_Combination of M by A37, A83;
v in {v} by TARSKI:def 1;
then L1 is Convex_Combination of B by A37;
then A85: Carrier L1 c= {v} by RLVECT_2:def 6;
then A86: ( Carrier L1 = {} or Carrier L1 = {v} ) by ZFMISC_1:33;
A87: for u being Element of V holds L . u = ((r * L1) + ((1 - r) * L2)) . u

proof

let u be Element of V; :: thesis:
A88: ((r * L1) + ((1 - r) * L2)) . u = ((r * L1) . u) + (((1 - r) * L2) . u) by RLVECT_2:def 10;

per cases ;

suppose A89: u in Carrier L ; :: thesis:

per cases ;

suppose A90: u = v ; :: thesis:

then u in {v} by TARSKI:def 1;
then not u in Carrier L2 by A46, XBOOLE_0:def 5;
then L2 . u = 0 by RLVECT_2:19;
then (1 - r) * (L2 . u) = 0 ;
then A91: ((1 - r) * L2) . u = 0 by RLVECT_2:def 11;
L1 . u = 1 by A86, A90, CONVEX1:21, CONVEX1:27;
then A92: r * (L1 . u) = r ;
L . u = r + 0 by A17, A19, A30, A90;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A92, A91, RLVECT_2:def 11; :: thesis:

end;

suppose u <> v ; :: thesis:

then A93: not u in Carrier L1 by A85, TARSKI:def 1;
then L1 . u = 0 by RLVECT_2:19;
then r * (L1 . u) = 0 ;
then A94: (r * L1) . u = 0 by RLVECT_2:def 11;
u in Carrier L2 by A52, A86, A89, A93, CONVEX1:21, XBOOLE_0:def 5;
then L2 . u = (1 / (1 - r)) * (L . u) by A2, A40, A46;
then (1 - r) * (L2 . u) = ((1 - r) * (1 / (1 - r))) * (L . u)
.= (1 / ((1 - r) / (1 - r))) * (L . u) by XCMPLX_1:81
.= 1 * (L . u) by A18, A47, A29, XCMPLX_1:51
.= L . u ;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A94, RLVECT_2:def 11; :: thesis:

end;

suppose A95: not u in Carrier L ; :: thesis:

then not u in Carrier L1 by A2, A15, A85, TARSKI:def 1;
then L1 . u = 0 by RLVECT_2:19;
then r * (L1 . u) = 0 ;
then A96: (r * L1) . u = 0 by RLVECT_2:def 11;
not u in Carrier L2 by A46, A95, XBOOLE_0:def 5;
then L2 . u = 0 by RLVECT_2:19;
then A97: (1 - r) * (L2 . u) = 0 ;
L . u = 0 + 0 by A95, RLVECT_2:19;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A88, A96, A97, RLVECT_2:def 11; :: thesis:

end;

take L1 ; :: thesis:
take L2 ; :: thesis:
take r ; :: thesis:
f . (len f) = L . (F . (len f)) by A19, A30;
then r <> 0 by A2, A17, A16, RLVECT_2:19;
hence ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) by A19, A30, A48, A86, A87, A84, CARD_1:30, CONVEX1:21, RLVECT_2:def 9; :: thesis: