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 = jj / 2 & L . v2 = jj / 2 ) by A1, RLVECT_4:38;
consider F being FinSequence of the carrier of V such that
A3: ( F is one-to-one & rng F = Carrier L ) and
Sum L = Sum (L (#) F) by RLVECT_2:def 8;
deffunc H₁( set ) -> set = L . (F . $1);
consider f being FinSequence such that
A4: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H₁(n) ) ) from FINSEQ_1:sch 2();
( v1 in Carrier L & v2 in Carrier L ) by A2, RLVECT_2:19;
then ( Carrier L c= {v1,v2} & {v1,v2} c= Carrier L ) by RLVECT_2:def 6, ZFMISC_1:32;
then A5: {v1,v2} = Carrier L by XBOOLE_0:def 10;
then A6: len F = 2 by A1, A3, FINSEQ_3:98;
then 2 in dom f by A4, FINSEQ_3:25;
then A7: f . 2 = L . (F . 2) by A4;
1 in dom f by A4, A6, FINSEQ_3:25;
then A8: f . 1 = L . (F . 1) by A4;

now :: 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

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

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:44;
then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44;
then f = <*jd*> ^ <*jd*> by FINSEQ_1:def 9;
then rng f = (rng <*(1 / 2)*>) \/ (rng <*jd*>) by FINSEQ_1:31
.= {jd} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A10: 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, A4, A6, A8, A7, A9, A11, FINSEQ_1:2, TARSKI:def 2; :: thesis: verum

end;

f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A9, FINSEQ_1:44;
then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77
.= 1 ;
then reconsider L = L as Convex_Combination of V by A3, A4, A10, CONVEX1:def 3;
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
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A5, RLVECT_2:def 6;
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

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 A12: ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:44;
then f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, FINSEQ_1:44;
then f = <*jd*> ^ <*jd*> by FINSEQ_1:def 9;
then rng f = (rng <*(1 / 2)*>) \/ (rng <*jd*>) by FINSEQ_1:31
.= {jd} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A13: 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 A14: 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, A4, A6, A8, A7, A12, A14, FINSEQ_1:2, TARSKI:def 2; :: thesis: verum

end;

f = <*(1 / 2),(1 / 2)*> by A2, A4, A6, A8, A7, A12, FINSEQ_1:44;
then Sum f = (1 / 2) + (1 / 2) by RVSUM_1:77
.= 1 ;
then reconsider L = L as Convex_Combination of V by A3, A4, A13, CONVEX1:def 3;
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
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A by A5, RLVECT_2:def 6;
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

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