let V be RealLinearSpace; :: thesis: for v, u being VECTOR of V

for A being Subset of V st v in conv A & u in conv A & v <> u holds

ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

let v, u be VECTOR of V; :: thesis: for A being Subset of V st v in conv A & u in conv A & v <> u holds

ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

let A be Subset of V; :: thesis: ( v in conv A & u in conv A & v <> u implies ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) )

reconsider Z = 0 as Real ;

assume that

A1: v in conv A and

A2: u in conv A and

A3: v <> u ; :: thesis: ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

reconsider A1 = A as non empty Subset of V by A1;

A4: conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

then consider Lv being Convex_Combination of A1 such that

A5: v = Sum Lv and

A6: Lv in ConvexComb V by A1;

set Cv = Carrier Lv;

A7: Carrier Lv c= A by RLVECT_2:def 6;

consider Lu being Convex_Combination of A1 such that

A8: u = Sum Lu and

Lu in ConvexComb V by A2, A4;

set Cu = Carrier Lu;

A9: Carrier Lu c= A by RLVECT_2:def 6;

then A10: (Carrier Lv) \/ (Carrier Lu) c= A by A7, XBOOLE_1:8;

for A being Subset of V st v in conv A & u in conv A & v <> u holds

ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

let v, u be VECTOR of V; :: thesis: for A being Subset of V st v in conv A & u in conv A & v <> u holds

ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

let A be Subset of V; :: thesis: ( v in conv A & u in conv A & v <> u implies ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v ) )

reconsider Z = 0 as Real ;

assume that

A1: v in conv A and

A2: u in conv A and

A3: v <> u ; :: thesis: ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

reconsider A1 = A as non empty Subset of V by A1;

A4: conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

then consider Lv being Convex_Combination of A1 such that

A5: v = Sum Lv and

A6: Lv in ConvexComb V by A1;

set Cv = Carrier Lv;

A7: Carrier Lv c= A by RLVECT_2:def 6;

consider Lu being Convex_Combination of A1 such that

A8: u = Sum Lu and

Lu in ConvexComb V by A2, A4;

set Cu = Carrier Lu;

A9: Carrier Lu c= A by RLVECT_2:def 6;

then A10: (Carrier Lv) \/ (Carrier Lu) c= A by A7, XBOOLE_1:8;

per cases
( not Carrier Lu c= Carrier Lv or Carrier Lu c= Carrier Lv )
;

end;

suppose
not Carrier Lu c= Carrier Lv
; :: thesis: ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

then consider p being object such that

A11: p in Carrier Lu and

A12: not p in Carrier Lv ;

reconsider p = p as Element of V by A11;

( Carrier Lv <> {} & Carrier Lv c= A \ {p} ) by A7, A12, CONVEX1:21, ZFMISC_1:34;

then reconsider Ap = A \ {p} as non empty Subset of V ;

Carrier Lv c= Ap by A7, A12, ZFMISC_1:34;

then reconsider LV = Lv as Linear_Combination of Ap by RLVECT_2:def 6;

take p ; :: thesis: ex w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

take w = v; :: thesis: ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

take Z ; :: thesis: ( p in A & w in conv (A \ {p}) & 0 <= Z & Z < 1 & (Z * u) + ((1 - Z) * w) = v )

A13: (Z * u) + ((1 - Z) * w) = (0. V) + (1 * w) by RLVECT_1:10

.= (0. V) + w by RLVECT_1:def 8

.= v ;

Sum LV in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A6;

hence ( p in A & w in conv (A \ {p}) & 0 <= Z & Z < 1 & (Z * u) + ((1 - Z) * w) = v ) by A5, A9, A11, A13, CONVEX3:5; :: thesis: verum

end;A11: p in Carrier Lu and

A12: not p in Carrier Lv ;

reconsider p = p as Element of V by A11;

( Carrier Lv <> {} & Carrier Lv c= A \ {p} ) by A7, A12, CONVEX1:21, ZFMISC_1:34;

then reconsider Ap = A \ {p} as non empty Subset of V ;

Carrier Lv c= Ap by A7, A12, ZFMISC_1:34;

then reconsider LV = Lv as Linear_Combination of Ap by RLVECT_2:def 6;

take p ; :: thesis: ex w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

take w = v; :: thesis: ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

take Z ; :: thesis: ( p in A & w in conv (A \ {p}) & 0 <= Z & Z < 1 & (Z * u) + ((1 - Z) * w) = v )

A13: (Z * u) + ((1 - Z) * w) = (0. V) + (1 * w) by RLVECT_1:10

.= (0. V) + w by RLVECT_1:def 8

.= v ;

Sum LV in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A6;

hence ( p in A & w in conv (A \ {p}) & 0 <= Z & Z < 1 & (Z * u) + ((1 - Z) * w) = v ) by A5, A9, A11, A13, CONVEX3:5; :: thesis: verum

suppose A14:
Carrier Lu c= Carrier Lv
; :: thesis: ex p, w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

defpred S_{1}[ set , set ] means for r being Real

for p being Element of V st r = $2 & p = $1 holds

( r < 0 & Lv . p <> Lu . p & ((r * Lu) + ((1 - r) * Lv)) . p = 0 );

set P = { r where r is Element of REAL : ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } ;

for r, s being Element of REAL st S_{1}[p,r] & S_{1}[p,s] holds

r = s

then consider p being Element of V such that

A20: Lu . p > Lv . p by A3, A5, A8, Th24;

A21: Lv . p <> 0

then A23: p in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def 3;

set r = (Lv . p) / ((Lv . p) - (Lu . p));

A24: ( (Lv . p) / ((Lv . p) - (Lu . p)) = ((Lv . p) - Z) / ((Lv . p) - (Lu . p)) & (Lv . p) - (Lu . p) < (Lu . p) - (Lu . p) ) by A20, XREAL_1:9;

Lv . p > 0 by A21, RLAFFIN1:62;

then S_{1}[p,(Lv . p) / ((Lv . p) - (Lu . p))]
by A24, Lm3;

then A25: (Lv . p) / ((Lv . p) - (Lu . p)) in { r where r is Element of REAL : ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) }
by A23;

A26: (Carrier Lv) \/ (Carrier Lu) is finite ;

{ r where r is Element of REAL : ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } is finite
from FRAENKEL:sch 28(A26, A16);

then reconsider P = { r where r is Element of REAL : ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } as non empty finite real-membered set by A15, A25, MEMBERED:def 3;

set M = max P;

max P in P by XXREAL_2:def 8;

then consider r being Element of REAL such that

A27: max P = r and

A28: ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) )
;

set Lw = (r * Lu) + ((1 - r) * Lv);

consider p being Element of V such that

A29: S_{1}[p,r]
and

A30: p in (Carrier Lv) \/ (Carrier Lu) by A28;

set w = (r * u) + ((1 - r) * v);

set R = (- r) / (1 - r);

A31: Sum ((r * Lu) + ((1 - r) * Lv)) = (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:1

.= (r * u) + (Sum ((1 - r) * Lv)) by A8, RLVECT_3:2

.= (r * u) + ((1 - r) * v) by A5, RLVECT_3:2 ;

A32: for z being Element of V holds 0 <= ((r * Lu) + ((1 - r) * Lv)) . z

then (r * Lu) + ((1 - r) * Lv) is Linear_Combination of A by RLVECT_2:38;

then A41: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A by RLVECT_2:def 6;

((r * Lu) + ((1 - r) * Lv)) . p = 0 by A29;

then not p in Carrier ((r * Lu) + ((1 - r) * Lv)) by RLVECT_2:19;

then A42: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A \ {p} by A41, ZFMISC_1:34;

A43: sum ((r * Lu) + ((1 - r) * Lv)) = (sum (r * Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:34

.= (r * (sum Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:35

.= (r * 1) + (sum ((1 - r) * Lv)) by RLAFFIN1:62

.= (r * 1) + ((1 - r) * (sum Lv)) by RLAFFIN1:35

.= (r * 1) + ((1 - r) * 1) by RLAFFIN1:62

.= 1 ;

then (r * Lu) + ((1 - r) * Lv) is convex by A32, RLAFFIN1:62;

then Carrier ((r * Lu) + ((1 - r) * Lv)) <> {} by CONVEX1:21;

then reconsider Ap = A \ {p} as non empty Subset of V by A42;

reconsider LW = (r * Lu) + ((1 - r) * Lv) as Linear_Combination of Ap by A42, RLVECT_2:def 6;

A44: LW is convex by A32, A43, RLAFFIN1:62;

then LW in ConvexComb V by CONVEX3:def 1;

then A45: Sum LW in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A44;

take p ; :: thesis: ex w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

take (r * u) + ((1 - r) * v) ; :: thesis: ex r being Real st

( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * ((r * u) + ((1 - r) * v))) = v )

take (- r) / (1 - r) ; :: thesis: ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= (- r) / (1 - r) & (- r) / (1 - r) < 1 & (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = v )

A46: 0 > r by A29;

then A47: ( 1 + (- r) > 0 + (- r) & (1 + (- r)) / (1 + (- r)) = 1 ) by XCMPLX_1:60, XREAL_1:6;

(((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = (((- r) / (1 - r)) * u) + ((((1 - r) / (1 - r)) - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) by A46, XCMPLX_1:60

.= (((- r) / (1 - r)) * u) + ((((1 - r) - (- r)) / (1 - r)) * ((r * u) + ((1 - r) * v))) by XCMPLX_1:120

.= (((- r) / (1 - r)) * u) + (((1 / (1 - r)) * (r * u)) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def 5

.= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def 7

.= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by RLVECT_1:def 7

.= (((- r) / (1 - r)) * u) + ((((r / (1 - r)) * 1) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by XCMPLX_1:75

.= (((- r) / (1 - r)) * u) + (((r / (1 - r)) * u) + (1 * v)) by A46, XCMPLX_1:87

.= ((((- r) / (1 - r)) * u) + ((r / (1 - r)) * u)) + (1 * v) by RLVECT_1:def 3

.= ((((- r) / (1 - r)) + (r / (1 - r))) * u) + (1 * v) by RLVECT_1:def 6

.= ((((- r) + r) / (1 - r)) * u) + (1 * v) by XCMPLX_1:62

.= ((0 / (1 - r)) * u) + v by RLVECT_1:def 8

.= (0. V) + v by RLVECT_1:10

.= v ;

hence ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= (- r) / (1 - r) & (- r) / (1 - r) < 1 & (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = v ) by A10, A30, A31, A45, A46, A47, CONVEX3:5, XREAL_1:74; :: thesis: verum

end;for p being Element of V st r = $2 & p = $1 holds

( r < 0 & Lv . p <> Lu . p & ((r * Lu) + ((1 - r) * Lv)) . p = 0 );

set P = { r where r is Element of REAL : ex p being Element of V st

( S

A15: now :: thesis: for x being object st x in { r where r is Element of REAL : ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } holds

x is real

A16:
for p being Element of V( S

x is real

let x be object ; :: thesis: ( x in { r where r is Element of REAL : ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } implies x is real )

assume x in { r where r is Element of REAL : ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) }
; :: thesis: x is real

then ex r being Element of REAL st

( r = x & ex p being Element of V st

( S_{1}[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) )
;

hence x is real ; :: thesis: verum

end;( S

assume x in { r where r is Element of REAL : ex p being Element of V st

( S

then ex r being Element of REAL st

( r = x & ex p being Element of V st

( S

hence x is real ; :: thesis: verum

for r, s being Element of REAL st S

r = s

proof

( sum Lu = 1 & sum Lv = 1 )
by RLAFFIN1:62;
let p be Element of V; :: thesis: for r, s being Element of REAL st S_{1}[p,r] & S_{1}[p,s] holds

r = s

let r, s be Element of REAL ; :: thesis: ( S_{1}[p,r] & S_{1}[p,s] implies r = s )

assume A17: S_{1}[p,r]
; :: thesis: ( not S_{1}[p,s] or r = s )

then A18: ((r * Lu) + ((1 - r) * Lv)) . p = 0 ;

A19: Lv . p <> Lu . p by A17;

assume S_{1}[p,s]
; :: thesis: r = s

then ((s * Lu) + ((1 - s) * Lv)) . p = 0 ;

then s = ((Lv . p) - 0) / ((Lv . p) - (Lu . p)) by A19, Lm3

.= r by A18, A19, Lm3 ;

hence r = s ; :: thesis: verum

end;r = s

let r, s be Element of REAL ; :: thesis: ( S

assume A17: S

then A18: ((r * Lu) + ((1 - r) * Lv)) . p = 0 ;

A19: Lv . p <> Lu . p by A17;

assume S

then ((s * Lu) + ((1 - s) * Lv)) . p = 0 ;

then s = ((Lv . p) - 0) / ((Lv . p) - (Lu . p)) by A19, Lm3

.= r by A18, A19, Lm3 ;

hence r = s ; :: thesis: verum

then consider p being Element of V such that

A20: Lu . p > Lv . p by A3, A5, A8, Th24;

A21: Lv . p <> 0

proof

then
p in Carrier Lv
;
assume A22:
Lv . p = 0
; :: thesis: contradiction

then not p in Carrier Lu by A14, RLVECT_2:19;

hence contradiction by A20, A22; :: thesis: verum

end;then not p in Carrier Lu by A14, RLVECT_2:19;

hence contradiction by A20, A22; :: thesis: verum

then A23: p in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def 3;

set r = (Lv . p) / ((Lv . p) - (Lu . p));

A24: ( (Lv . p) / ((Lv . p) - (Lu . p)) = ((Lv . p) - Z) / ((Lv . p) - (Lu . p)) & (Lv . p) - (Lu . p) < (Lu . p) - (Lu . p) ) by A20, XREAL_1:9;

Lv . p > 0 by A21, RLAFFIN1:62;

then S

then A25: (Lv . p) / ((Lv . p) - (Lu . p)) in { r where r is Element of REAL : ex p being Element of V st

( S

A26: (Carrier Lv) \/ (Carrier Lu) is finite ;

{ r where r is Element of REAL : ex p being Element of V st

( S

then reconsider P = { r where r is Element of REAL : ex p being Element of V st

( S

set M = max P;

max P in P by XXREAL_2:def 8;

then consider r being Element of REAL such that

A27: max P = r and

A28: ex p being Element of V st

( S

set Lw = (r * Lu) + ((1 - r) * Lv);

consider p being Element of V such that

A29: S

A30: p in (Carrier Lv) \/ (Carrier Lu) by A28;

set w = (r * u) + ((1 - r) * v);

set R = (- r) / (1 - r);

A31: Sum ((r * Lu) + ((1 - r) * Lv)) = (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:1

.= (r * u) + (Sum ((1 - r) * Lv)) by A8, RLVECT_3:2

.= (r * u) + ((1 - r) * v) by A5, RLVECT_3:2 ;

A32: for z being Element of V holds 0 <= ((r * Lu) + ((1 - r) * Lv)) . z

proof

( r * Lu is Linear_Combination of A & (1 - r) * Lv is Linear_Combination of A )
by RLVECT_2:44;
let z be Element of V; :: thesis: 0 <= ((r * Lu) + ((1 - r) * Lv)) . z

A33: ((Z * Lu) + ((1 - Z) * Lv)) . z = ((Z * Lu) . z) + (((1 - Z) * Lv) . z) by RLVECT_2:def 10

.= (Z * (Lu . z)) + (((1 - Z) * Lv) . z) by RLVECT_2:def 11

.= (Z * (Lu . z)) + ((1 - 0) * (Lv . z)) by RLVECT_2:def 11

.= Lv . z ;

assume A34: 0 > ((r * Lu) + ((1 - r) * Lv)) . z ; :: thesis: contradiction

A35: ((r * Lu) + ((1 - r) * Lv)) . z = ((r * Lu) . z) + (((1 - r) * Lv) . z) by RLVECT_2:def 10

.= (r * (Lu . z)) + (((1 - r) * Lv) . z) by RLVECT_2:def 11

.= (r * (Lu . z)) + ((1 - r) * (Lv . z)) by RLVECT_2:def 11 ;

A36: Lv . z <> 0

then A38: z in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def 3;

Lv . z >= 0 by RLAFFIN1:62;

then consider rs being Real such that

A39: ((rs * Lu) + ((1 - rs) * Lv)) . z = 0 and

A40: ( r <= 0 implies ( r <= rs & rs <= 0 ) ) and

( 0 <= r implies ( 0 <= rs & rs <= r ) ) by A33, A34, Th25;

reconsider rs = rs as Element of REAL by XREAL_0:def 1;

rs <> 0 by A33, A36, A39;

then S_{1}[z,rs]
by A29, A34, A35, A39, A40, RLAFFIN1:62;

then rs in P by A38;

then rs <= r by A27, XXREAL_2:def 8;

then rs = r by A28, A40, XXREAL_0:1;

hence contradiction by A34, A39; :: thesis: verum

end;A33: ((Z * Lu) + ((1 - Z) * Lv)) . z = ((Z * Lu) . z) + (((1 - Z) * Lv) . z) by RLVECT_2:def 10

.= (Z * (Lu . z)) + (((1 - Z) * Lv) . z) by RLVECT_2:def 11

.= (Z * (Lu . z)) + ((1 - 0) * (Lv . z)) by RLVECT_2:def 11

.= Lv . z ;

assume A34: 0 > ((r * Lu) + ((1 - r) * Lv)) . z ; :: thesis: contradiction

A35: ((r * Lu) + ((1 - r) * Lv)) . z = ((r * Lu) . z) + (((1 - r) * Lv) . z) by RLVECT_2:def 10

.= (r * (Lu . z)) + (((1 - r) * Lv) . z) by RLVECT_2:def 11

.= (r * (Lu . z)) + ((1 - r) * (Lv . z)) by RLVECT_2:def 11 ;

A36: Lv . z <> 0

proof

then
z in Carrier Lv
;
assume A37:
Lv . z = 0
; :: thesis: contradiction

then not z in Carrier Lu by A14, RLVECT_2:19;

then Lu . z = 0 ;

hence contradiction by A34, A35, A37; :: thesis: verum

end;then not z in Carrier Lu by A14, RLVECT_2:19;

then Lu . z = 0 ;

hence contradiction by A34, A35, A37; :: thesis: verum

then A38: z in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def 3;

Lv . z >= 0 by RLAFFIN1:62;

then consider rs being Real such that

A39: ((rs * Lu) + ((1 - rs) * Lv)) . z = 0 and

A40: ( r <= 0 implies ( r <= rs & rs <= 0 ) ) and

( 0 <= r implies ( 0 <= rs & rs <= r ) ) by A33, A34, Th25;

reconsider rs = rs as Element of REAL by XREAL_0:def 1;

rs <> 0 by A33, A36, A39;

then S

then rs in P by A38;

then rs <= r by A27, XXREAL_2:def 8;

then rs = r by A28, A40, XXREAL_0:1;

hence contradiction by A34, A39; :: thesis: verum

then (r * Lu) + ((1 - r) * Lv) is Linear_Combination of A by RLVECT_2:38;

then A41: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A by RLVECT_2:def 6;

((r * Lu) + ((1 - r) * Lv)) . p = 0 by A29;

then not p in Carrier ((r * Lu) + ((1 - r) * Lv)) by RLVECT_2:19;

then A42: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A \ {p} by A41, ZFMISC_1:34;

A43: sum ((r * Lu) + ((1 - r) * Lv)) = (sum (r * Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:34

.= (r * (sum Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:35

.= (r * 1) + (sum ((1 - r) * Lv)) by RLAFFIN1:62

.= (r * 1) + ((1 - r) * (sum Lv)) by RLAFFIN1:35

.= (r * 1) + ((1 - r) * 1) by RLAFFIN1:62

.= 1 ;

then (r * Lu) + ((1 - r) * Lv) is convex by A32, RLAFFIN1:62;

then Carrier ((r * Lu) + ((1 - r) * Lv)) <> {} by CONVEX1:21;

then reconsider Ap = A \ {p} as non empty Subset of V by A42;

reconsider LW = (r * Lu) + ((1 - r) * Lv) as Linear_Combination of Ap by A42, RLVECT_2:def 6;

A44: LW is convex by A32, A43, RLAFFIN1:62;

then LW in ConvexComb V by CONVEX3:def 1;

then A45: Sum LW in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A44;

take p ; :: thesis: ex w being VECTOR of V ex r being Real st

( p in A & w in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * w) = v )

take (r * u) + ((1 - r) * v) ; :: thesis: ex r being Real st

( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= r & r < 1 & (r * u) + ((1 - r) * ((r * u) + ((1 - r) * v))) = v )

take (- r) / (1 - r) ; :: thesis: ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= (- r) / (1 - r) & (- r) / (1 - r) < 1 & (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = v )

A46: 0 > r by A29;

then A47: ( 1 + (- r) > 0 + (- r) & (1 + (- r)) / (1 + (- r)) = 1 ) by XCMPLX_1:60, XREAL_1:6;

(((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = (((- r) / (1 - r)) * u) + ((((1 - r) / (1 - r)) - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) by A46, XCMPLX_1:60

.= (((- r) / (1 - r)) * u) + ((((1 - r) - (- r)) / (1 - r)) * ((r * u) + ((1 - r) * v))) by XCMPLX_1:120

.= (((- r) / (1 - r)) * u) + (((1 / (1 - r)) * (r * u)) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def 5

.= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def 7

.= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by RLVECT_1:def 7

.= (((- r) / (1 - r)) * u) + ((((r / (1 - r)) * 1) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by XCMPLX_1:75

.= (((- r) / (1 - r)) * u) + (((r / (1 - r)) * u) + (1 * v)) by A46, XCMPLX_1:87

.= ((((- r) / (1 - r)) * u) + ((r / (1 - r)) * u)) + (1 * v) by RLVECT_1:def 3

.= ((((- r) / (1 - r)) + (r / (1 - r))) * u) + (1 * v) by RLVECT_1:def 6

.= ((((- r) + r) / (1 - r)) * u) + (1 * v) by XCMPLX_1:62

.= ((0 / (1 - r)) * u) + v by RLVECT_1:def 8

.= (0. V) + v by RLVECT_1:10

.= v ;

hence ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= (- r) / (1 - r) & (- r) / (1 - r) < 1 & (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = v ) by A10, A30, A31, A45, A46, A47, CONVEX3:5, XREAL_1:74; :: thesis: verum