let V be RealLinearSpace; :: thesis:
let M be non empty Subset of V; :: thesis:
let L be Convex_Combination of M; :: thesis:
assume A1: card (Carrier L) >= 2 ; :: thesis:
consider F being FinSequence of the carrier of V such that
A2: ( 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 ) ) ) ) by CONVEX1:def 3;
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;
A4: for n, m being Element of NAT st 1 <= n & n < m & m <= len F holds
F . n <> F . m

proof

let n, m be Element of NAT ; :: thesis:
assume A5: ( 1 <= n & n < m & m <= len F ) ; :: thesis:
assume A6: F . n = F . m ; :: thesis:
( n <= len F & 1 <= m ) by A5, XXREAL_0:2;
then ( n in Seg (len F) & m in Seg (len F) ) by A5, FINSEQ_1:3;
then ( n in dom F & m in dom F ) by FINSEQ_1:def 3;
hence contradiction by A2, A5, A6, FUNCT_1:def 8; :: thesis:

end;

then A7: len F >= 2 by A1, A2, GRAPH_5:10;
len F >= 1 + 1 by A1, A2, A4, GRAPH_5:10;
then A8: (len F) - 1 >= 1 by XREAL_1:21;
consider i being Nat such that
A9: len F = i + 1 by A7, NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A10: (len F) - 1 = i by A9;
set v = F . (len F);
1 <= len F by A7, XXREAL_0:2;
then A11: len F in dom F by FINSEQ_3:27;
then A12: ( F . (len F) in rng F & rng F c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:12;
then reconsider v = F . (len F) as VECTOR of V ;
consider L1 being Convex_Combination of V such that
A13: ( Sum L1 = v & ( for A being non empty Subset of V st v in A holds
L1 is Convex_Combination of A ) ) by Th1;
A14: ( v in Carrier L & Carrier L c= M ) by A2, A11, FUNCT_1:12, RLVECT_2:def 8;
then reconsider L1 = L1 as Convex_Combination of M by A13;
1 <= len f by A3, A7, XXREAL_0:2;
then len f in Seg (len f) by FINSEQ_1:3;
then A15: len f in dom f by FINSEQ_1:def 3;
then ( f . (len f) in rng f & rng f c= REAL ) by FUNCT_1:12;
then reconsider r = f . (len f) as Real ;
A16: ( 0 < r & r < 1 )

proof

A17: ( f . (len f) = L . (F . (len f)) & f . (len f) >= 0 ) by A3, A15;
F . (len F) in rng F by A11, FUNCT_1:12;
then A18: ( r <> 0 & r >= 0 ) by A2, A3, A17, RLVECT_2:28;
A19: f = (f | i) ^ (f /^ i) by RFINSEQ:21;
f /^ i = <*(f /. (len f))*> by A3, A9, FINSEQ_5:33
.= <*(f . (len f))*> by A15, PARTFUN1:def 8 ;
then Sum f = (Sum (f | i)) + r by A19, RVSUM_1:104;
then A20: Sum (f | i) = 1 - r by A3;
Sum (f | i) > 0

proof

A21: for k being Nat st k in dom (f | i) holds
0 <= (f | i) . k

proof

end;

ex k being Element of NAT st
( k in dom (f | i) & 0 < (f | i) . k )

proof

A24: 1 in Seg i by A8, A9, FINSEQ_1:3;
1 <= len f by A3, A7, XXREAL_0:2;
then A25: 1 in Seg (len f) by FINSEQ_1:3;
then A26: 1 in dom f by FINSEQ_1:def 3;
then A27: 1 in dom (f | (Seg i)) by A24, RELAT_1:86;
then A28: 1 in dom (f | i) by FINSEQ_1:def 15;
f | i = f | (Seg i) by FINSEQ_1:def 15;
then A29: (f | i) . 1 = f . 1 by A27, FUNCT_1:70
.= L . (F . 1) by A3, A26 ;
1 in dom F by A3, A25, FINSEQ_1:def 3;
then F . 1 in rng F by FUNCT_1:12;
then A30: L . (F . 1) <> 0 by A2, RLVECT_2:28;
(f | i) . 1 >= 0 by A21, A28;
hence ex k being Element of NAT st
( k in dom (f | i) & 0 < (f | i) . k ) by A28, A29, A30; :: thesis:

end;

hence Sum (f | i) > 0 by A21, RVSUM_1:115; :: thesis:

end;

then 1 > r + 0 by A20, XREAL_1:22;
hence ( 0 < r & r < 1 ) by A18; :: thesis:

end;

set r' = 1 / (1 - r);
1 > r + 0 by A16;
then A31: 1 - r > 0 by XREAL_1:22;
then A32: 1 / (1 - r) > 0 by XREAL_1:141;
defpred S₁[ set , set ] means ( ( $1 in (rng F) \ {v} implies $2 = (1 / (1 - r)) * (L . $1) ) & ( not $1 in (rng F) \ {v} implies $2 = 0 ) );
A34: for x being set st x in the carrier of V holds
ex y being set st S₁[x,y]

proof

let x be set ; :: 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 set st S₁[x,y] ; :: thesis:

end;

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

proof

let y be set ; :: thesis:
assume y in rng L2 ; :: thesis:
then consider x being set such that
A36: ( x in dom L2 & y = L2 . x ) by FUNCT_1:def 5;

per cases ;

suppose A37: 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 A35, A36, A37
.= ((1 / (1 - r)) * L) . x by RLVECT_2:def 13 ;
hence y in REAL ; :: thesis:

end;

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

then y = 0 by A35, A36;
hence y in REAL ; :: thesis:

end;

then rng L2 c= REAL by TARSKI:def 3;
then A38: L2 is Element of Funcs the carrier of V,REAL by A35, 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, A35; :: thesis:

end;

then reconsider L2 = L2 as Linear_Combination of V by A38, RLVECT_2:def 5;
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

let n, m be Element of NAT ; :: thesis:
assume that
A39: n in dom (F | i) and
A40: m in dom (F | i) and
A41: (F | i) /. n = (F | i) /. m ; :: thesis:
A42: dom (F | i) c= dom F by FINSEQ_5:20;
F /. n = (F | i) /. n by A39, FINSEQ_4:85
.= F /. m by A40, A41, FINSEQ_4:85 ;
hence n = m by A2, A39, A40, A42, PARTFUN2:17; :: thesis:

end;

then A43: F | i is one-to-one by PARTFUN2:16;
A44: Carrier L2 = (Carrier L) \ {v}

proof

for u being set st u in Carrier L2 holds
u in (Carrier L) \ {v}

proof

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

end;

then A46: Carrier L2 c= (Carrier L) \ {v} by TARSKI:def 3;
for u being set st u in (Carrier L) \ {v} holds
u in Carrier L2

proof

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

end;

then (Carrier L) \ {v} c= Carrier L2 by TARSKI:def 3;
hence Carrier L2 = (Carrier L) \ {v} by A46, XBOOLE_0:def 10; :: thesis:

end;

then ( Carrier L2 c= Carrier L & Carrier L c= M ) by RLVECT_2:def 8, XBOOLE_1:36;
then Carrier L2 c= M by XBOOLE_1:1;
then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def 8;
A50: rng (F | i) = Carrier L2

proof

F = (F | i) ^ (F /^ i) by RFINSEQ:21;
then A51: Carrier L = (rng (F | i)) \/ (rng (F /^ i)) by A2, FINSEQ_1:44;
rng (F | i) misses rng (F /^ i) by A2, FINSEQ_5:37;
then A52: (Carrier L) \ (rng (F /^ i)) = rng (F | i) by A51, XBOOLE_1:88;
F /^ i = <*(F /. (len F))*> by A9, FINSEQ_5:33
.= <*(F . (len F))*> by A11, PARTFUN1:def 8 ;
hence rng (F | i) = Carrier L2 by A44, A52, FINSEQ_1:55; :: thesis:

end;

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();
for y being set st y in rng f2 holds
y in REAL

proof

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

end;

then rng f2 c= REAL by TARSKI:def 3;
then reconsider f2 = f2 as FinSequence of REAL by FINSEQ_1:def 4;
( Sum f2 = 1 & ( for n being Nat st n in dom f2 holds
( f2 . n = L2 . ((F | i) . n) & f2 . n >= 0 ) ) )

proof

A58: i <= len F by A9, NAT_1:12;
A59: dom f2 = Seg (len (F | i)) by A53, FINSEQ_1:def 3;
then A60: dom f2 = Seg i by A9, FINSEQ_1:80, NAT_1:12
.= Seg (len (f | i)) by A3, A58, FINSEQ_1:80
.= dom (f | i) by FINSEQ_1:def 3 ;
then A61: dom f2 = dom ((1 / (1 - r)) * (f | i)) by VALUED_1:def 5;
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)) & f | i = f | (Seg i) ) by A60, A63, FINSEQ_1:def 15;
then A65: ( k in (dom f) /\ (Seg i) & (f | i) . k = f . k ) by FUNCT_1:70, RELAT_1:90;
then A66: k in dom f by XBOOLE_0:def 4;
then A67: (f | i) . k = L . (F . k) by A3, A65;
A68: k in dom (F | i) by A59, A63, FINSEQ_1:def 3;
A69: F | i = F | (Seg i) by FINSEQ_1:def 15;
then A70: (F | i) . k = F . k by A68, FUNCT_1:70;
A71: (f | i) . k = L . ((F | i) . k) by A67, A68, A69, FUNCT_1:70;
(F | i) . k in rng (F | i) by A68, FUNCT_1:12;
then reconsider w = (F | i) . k as Element of V by A50;
A72: not w in {v}

proof

assume w in {v} ; :: thesis:
then A73: F . k = v by A70, TARSKI:def 1;
dom (F | (Seg i)) c= dom F by RELAT_1:89;
then A74: k = len F by A2, A11, A68, A69, A73, FUNCT_1:def 8;
( k <= len (F | i) & len (F | i) <= i ) by A59, A63, FINSEQ_1:3, FINSEQ_5:19;
then k <= i by XXREAL_0:2;
then k + 1 <= len F by A10, XREAL_1:21;
hence contradiction by A74, NAT_1:13; :: thesis:

end;

per cases ;

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

then A75: L2 . w = (1 / (1 - r)) * (L . w) by A35
.= (1 / (1 - r)) * ((f | i) . k) by A67, A68, A69, FUNCT_1:70
.= ((1 / (1 - r)) * (f | i)) . k by RVSUM_1:66 ;
f . k >= 0 by A3, A66;
then (1 / (1 - r)) * ((f | i) . k) >= 0 by A32, A65;
hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A64, A75, RVSUM_1:66; :: thesis:

end;

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

then A77: not w in rng F by A72, XBOOLE_0:def 5;
A78: f2 . k = 0 by A35, A64, A76;
L . w = 0 by A2, A77, RLVECT_2:28;
then (1 / (1 - r)) * ((f | i) . k) = 0 by A71;
hence ( f2 . k = ((1 / (1 - r)) * (f | i)) . k & f2 . k >= 0 ) by A78, RVSUM_1:66; :: thesis:

end;

then for k being Nat st k in dom f2 holds
f2 . k = ((1 / (1 - r)) * (f | i)) . k ;
then A79: f2 = (1 / (1 - r)) * (f | i) by A61, FINSEQ_1:17;
A80: f = (f | i) ^ (f /^ i) by RFINSEQ:21;
f /^ i = <*(f /. (len f))*> by A3, A9, FINSEQ_5:33
.= <*(f . (len f))*> by A15, PARTFUN1:def 8 ;
then Sum f = (Sum (f | i)) + r by A80, RVSUM_1:104;
hence Sum f2 = (1 / (1 - r)) * (1 - r) by A3, A79, RVSUM_1:117
.= 1 / ((1 - r) / (1 - r)) by XCMPLX_1:82
.= 1 / 1 by A31, XCMPLX_1:60
.= 1 ;
:: thesis:
thus for n being Nat st n in dom f2 holds
( f2 . n = L2 . ((F | i) . n) & f2 . n >= 0 ) by A53, A62; :: thesis:

end;

then reconsider L2 = L2 as Convex_Combination of M by A43, A50, A53, CONVEX1:def 3;
A81: v in {v} by TARSKI:def 1;
reconsider B = {v} as non empty Subset of V ;
L1 is Convex_Combination of B by A13, A81;
then A82: Carrier L1 c= {v} by RLVECT_2:def 8;
then A83: ( Carrier L1 = {} or Carrier L1 = {v} ) by ZFMISC_1:39;
A84: for u being Element of V holds L . u = ((r * L1) + ((1 - r) * L2)) . u

proof

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

per cases ;

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

per cases ;

suppose A87: u = v ; :: thesis:

then L1 . u = 1 by A83, CONVEX1:21, CONVEX1:27;
then A88: r * (L1 . u) = r ;
u in {v} by A87, TARSKI:def 1;
then not u in Carrier L2 by A44, XBOOLE_0:def 5;
then L2 . u = 0 by RLVECT_2:28;
then (1 - r) * (L2 . u) = 0 ;
then A89: ((1 - r) * L2) . u = 0 by RLVECT_2:def 13;
L . u = r + 0 by A3, A15, A87;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A85, A88, A89, RLVECT_2:def 13; :: thesis:

end;

suppose u <> v ; :: thesis:

then A90: not u in Carrier L1 by A82, TARSKI:def 1;
then L1 . u = 0 by RLVECT_2:28;
then r * (L1 . u) = 0 ;
then A91: (r * L1) . u = 0 by RLVECT_2:def 13;
u in Carrier L2 by A44, A83, A86, A90, CONVEX1:21, XBOOLE_0:def 5;
then L2 . u = (1 / (1 - r)) * (L . u) by A2, A35, A44;
then (1 - r) * (L2 . u) = ((1 - r) * (1 / (1 - r))) * (L . u)
.= (1 / ((1 - r) / (1 - r))) * (L . u) by XCMPLX_1:82
.= 1 * (L . u) by A31, XCMPLX_1:51
.= L . u ;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A85, A91, RLVECT_2:def 13; :: thesis:

end;

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

then A93: L . u = 0 + 0 by RLVECT_2:28;
not u in Carrier L1 by A2, A12, A82, A92, TARSKI:def 1;
then L1 . u = 0 by RLVECT_2:28;
then r * (L1 . u) = 0 ;
then A94: (r * L1) . u = 0 by RLVECT_2:def 13;
not u in Carrier L2 by A44, A92, XBOOLE_0:def 5;
then L2 . u = 0 by RLVECT_2:28;
then (1 - r) * (L2 . u) = 0 ;
hence L . u = ((r * L1) + ((1 - r) * L2)) . u by A85, A93, A94, RLVECT_2:def 13; :: thesis:

end;

take L1 ; :: thesis:
take L2 ; :: thesis:
take r ; :: thesis:
{v} c= Carrier L by A14, ZFMISC_1:37;
then card (Carrier L2) = (card (Carrier L)) - (card {v}) by A44, CARD_2:63;
hence ( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) by A16, A83, A84, CARD_1:50, CONVEX1:21, RLVECT_2:def 11; :: thesis: