let V be RealLinearSpace; :: thesis: for v1, v2, v3 being VECTOR of V st v1 <> v2 & v1 <> v3 & v2 <> v3 holds
ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A
let v1, v2, v3 be VECTOR of V; :: thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A )
assume that
A1: v1 <> v2 and
A2: v1 <> v3 and
A3: v2 <> v3 ; :: thesis: ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A
consider L being Linear_Combination of {v1,v2,v3} such that
A4: ( L . v1 = 1 / 3 & L . v2 = 1 / 3 & L . v3 = 1 / 3 ) from RLVECT_4:sch 4(A1, A2, A3);
A5: Carrier L c= {v1,v2,v3} by RLVECT_2:def 8;
for x being set st x in {v1,v2,v3} holds
x in Carrier L

proof

let x be set ; :: thesis: ( x in {v1,v2,v3} implies x in Carrier L )
assume A6: x in {v1,v2,v3} ; :: thesis: x in Carrier L
then reconsider x = x as VECTOR of V ;
( x = v1 or x = v2 or x = v3 ) by A6, ENUMSET1:def 1;
hence x in Carrier L by A4, RLVECT_2:28; :: thesis: verum

end;

then {v1,v2,v3} c= Carrier L by TARSKI:def 3;
then A7: {v1,v2,v3} = Carrier L by A5, XBOOLE_0:def 10;
consider F being FinSequence of the carrier of V such that
A8: ( 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
A9: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A10: len F = 3 by A1, A2, A3, A7, A8, FINSEQ_3:110;
then ( 1 in dom f & 2 in dom f & 3 in dom f ) by A9, FINSEQ_3:27;
then A11: ( f . 1 = L . (F . 1) & f . 2 = L . (F . 2) & f . 3 = L . (F . 3) ) by A9;

now

per cases ( F = <*v1,v2,v3*> or F = <*v1,v3,v2*> or F = <*v2,v1,v3*> or F = <*v2,v3,v1*> or F = <*v3,v1,v2*> or F = <*v3,v2,v1*> ) by A1, A2, A3, A7, A8, CONVEX1:31;

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

then A12: ( F . 1 = v1 & F . 2 = v2 & F . 3 = v3 ) by FINSEQ_1:62;
rng f c= REAL

proof

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A12, FINSEQ_1:62;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def 10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= {(1 / 3)} 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 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A12, FINSEQ_1:62;
then A13: Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:108
.= 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 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 A4, A9, A10, A11, A12, A14, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A8, A9, A13, CONVEX1:def 3;
A15: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7, 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,v3} 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,v3} c= A holds
L is Convex_Combination of A by A15; :: thesis: verum

end;

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

then A16: ( F . 1 = v1 & F . 2 = v3 & F . 3 = v2 ) by FINSEQ_1:62;
rng f c= REAL

proof

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A16, FINSEQ_1:62;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def 10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= {(1 / 3)} 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 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A16, FINSEQ_1:62;
then A17: Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:108
.= 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 A18: 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 A4, A9, A10, A11, A16, A18, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A8, A9, A17, CONVEX1:def 3;
A19: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7, 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,v3} 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,v3} c= A holds
L is Convex_Combination of A by A19; :: thesis: verum

end;

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

then A20: ( F . 1 = v2 & F . 2 = v1 & F . 3 = v3 ) by FINSEQ_1:62;
rng f c= REAL

proof

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A20, FINSEQ_1:62;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def 10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= {(1 / 3)} 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 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A20, FINSEQ_1:62;
then A21: Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:108
.= 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 A22: 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 A4, A9, A10, A11, A20, A22, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A8, A9, A21, CONVEX1:def 3;
A23: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7, 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,v3} 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,v3} c= A holds
L is Convex_Combination of A by A23; :: thesis: verum

end;

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

then A24: ( F . 1 = v2 & F . 2 = v3 & F . 3 = v1 ) by FINSEQ_1:62;
rng f c= REAL

proof

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A24, FINSEQ_1:62;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def 10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= {(1 / 3)} 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 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A24, FINSEQ_1:62;
then A25: Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:108
.= 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 A26: 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 A4, A9, A10, A11, A24, A26, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A8, A9, A25, CONVEX1:def 3;
A27: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7, 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,v3} 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,v3} c= A holds
L is Convex_Combination of A by A27; :: thesis: verum

end;

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

then A28: ( F . 1 = v3 & F . 2 = v1 & F . 3 = v2 ) by FINSEQ_1:62;
rng f c= REAL

proof

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A28, FINSEQ_1:62;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def 10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= {(1 / 3)} 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 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A28, FINSEQ_1:62;
then A29: Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:108
.= 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 A30: 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 A4, A9, A10, A11, A28, A30, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A8, A9, A29, CONVEX1:def 3;
A31: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7, 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,v3} 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,v3} c= A holds
L is Convex_Combination of A by A31; :: thesis: verum

end;

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

then A32: ( F . 1 = v3 & F . 2 = v2 & F . 3 = v1 ) by FINSEQ_1:62;
rng f c= REAL

proof

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A32, FINSEQ_1:62;
then f = (<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> by FINSEQ_1:def 10;
then rng f = (rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= ((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:44
.= {(1 / 3)} 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 / 3),(1 / 3),(1 / 3)*> by A4, A9, A10, A11, A32, FINSEQ_1:62;
then A33: Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:108
.= 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 A34: 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 A4, A9, A10, A11, A32, A34, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A8, A9, A33, CONVEX1:def 3;
A35: for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A7, 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,v3} 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,v3} c= A holds
L is Convex_Combination of A by A35; :: 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,v3} c= A holds
L is Convex_Combination of A ; :: thesis: verum