let V be RealLinearSpace; :: thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds
ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
let v1, v2 be VECTOR of V; :: thesis: ( v1 <> v2 implies ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A )
assume A1: v1 <> v2 ; :: thesis: ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
consider L being Linear_Combination of {v1,v2} such that
A2: ( L . v1 = 1 / 2 & L . v2 = 1 / 2 ) from RLVECT_4:sch 3(A1);
A3: Carrier L c= {v1,v2} by RLVECT_2:def 8;
( v1 in Carrier L & v2 in Carrier L ) by A2, RLVECT_2:28;
then {v1,v2} c= Carrier L by ZFMISC_1:38;
then A4: {v1,v2} = Carrier L by A3, XBOOLE_0:def 10;
consider F being FinSequence of the carrier of V such that
A5: ( F is one-to-one & rng F = Carrier L & Sum L = Sum (L (#) F) ) by RLVECT_2:def 10;
deffunc H₁( set ) -> set = L . (F . $1);
consider f being FinSequence such that
A6: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A7: len F = 2 by A1, A4, A5, FINSEQ_3:107;
then ( 1 in dom f & 2 in dom f ) by A6, FINSEQ_3:27;
then A8: ( f . 1 = L . (F . 1) & f . 2 = L . (F . 2) ) by A6;

now

per cases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A4, A5, FINSEQ_3:108;

suppose F = <*v1,v2*> ; :: thesis: ex L, L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A

then A9: ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:61;
rng f c= REAL

proof

f = <*(1 / 2),(1 / 2)*> by A2, A6, A7, A8, A9, FINSEQ_1:61;
then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def 9;
then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:44
.= {(1 / 2)} by FINSEQ_1:55 ;
hence rng f c= REAL ; :: thesis: verum

end;

then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
f = <*(1 / 2),(1 / 2)*> by A2, A6, A7, A8, A9, FINSEQ_1:61;
then A10: Sum f = (1 / 2) + (1 / 2) by RVSUM_1:107
.= 1 ;
for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )

proof

let n be Nat; :: thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A11: n in dom f ; :: thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def 3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A6, A7, A8, A9, A11, FINSEQ_1:4, TARSKI:def 2; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A5, A6, A10, CONVEX1:def 3;
A12: for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A4, RLVECT_2:def 8;
take L = L; :: thesis: ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
thus ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A12; :: thesis: verum

end;

suppose F = <*v2,v1*> ; :: thesis: ex L, L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A

then A13: ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:61;
rng f c= REAL

proof

f = <*(1 / 2),(1 / 2)*> by A2, A6, A7, A8, A13, FINSEQ_1:61;
then f = <*(1 / 2)*> ^ <*(1 / 2)*> by FINSEQ_1:def 9;
then rng f = (rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) by FINSEQ_1:44
.= {(1 / 2)} by FINSEQ_1:55 ;
hence rng f c= REAL ; :: thesis: verum

end;

then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
f = <*(1 / 2),(1 / 2)*> by A2, A6, A7, A8, A13, FINSEQ_1:61;
then A14: Sum f = (1 / 2) + (1 / 2) by RVSUM_1:107
.= 1 ;
for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )

proof

let n be Nat; :: thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A15: n in dom f ; :: thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def 3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A2, A6, A7, A8, A13, A15, FINSEQ_1:4, TARSKI:def 2; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A5, A6, A14, CONVEX1:def 3;
A16: for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A4, RLVECT_2:def 8;
take L = L; :: thesis: ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
thus ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A16; :: thesis: verum

end;

end;

end;

hence ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A ; :: thesis: verum