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 = jj / 3 & L . v2 = jj / 3 & L . v3 = jj / 3 ) by A1, A2, A3, RLVECT_4:39;
consider F being FinSequence of the carrier of V such that
A5: ( 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
A6: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H₁(n) ) ) from FINSEQ_1:sch 2();
for x being object st x in {v1,v2,v3} holds
x in Carrier L

proof

let x be object ; :: thesis: ( x in {v1,v2,v3} implies x in Carrier L )
assume A7: 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 A7, ENUMSET1:def 1;
hence x in Carrier L by A4, RLVECT_2:19; :: thesis: verum

end;

then ( Carrier L c= {v1,v2,v3} & {v1,v2,v3} c= Carrier L ) by RLVECT_2:def 6;
then A8: {v1,v2,v3} = Carrier L by XBOOLE_0:def 10;
then A9: len F = 3 by A1, A2, A3, A5, FINSEQ_3:101;
then 2 in dom f by A6, FINSEQ_3:25;
then A10: f . 2 = L . (F . 2) by A6;
3 in dom f by A6, A9, FINSEQ_3:25;
then A11: f . 3 = L . (F . 3) by A6;
1 in dom f by A6, A9, FINSEQ_3:25;
then A12: f . 1 = L . (F . 1) by A6;

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

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, A8, A5, CONVEX1:31;

suppose A13: 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 A14: F . 3 = v3 by FINSEQ_1:45;
A15: ( F . 1 = v1 & F . 2 = v2 ) by A13, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A14, FINSEQ_1:45;
then f = (<*jt*> ^ <*jt*>) ^ <*jt*> by FINSEQ_1:def 10;
then rng f = (rng (<*jt*> ^ <*jt*>)) \/ (rng <*(1 / 3)*>) by FINSEQ_1:31
.= ((rng <*(1 / 3)*>) \/ (rng <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= {jt} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A16: 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 A17: 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, A6, A9, A12, A10, A11, A15, A14, A17, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A15, A14, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A16, 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,v3} c= A holds
L is Convex_Combination of A
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def 6;
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

end;

suppose A18: 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 A19: F . 3 = v2 by FINSEQ_1:45;
A20: ( F . 1 = v1 & F . 2 = v3 ) by A18, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A19, FINSEQ_1:45;
then f = (<*jt*> ^ <*jt*>) ^ <*jt*> by FINSEQ_1:def 10;
then rng f = (rng (<*jt*> ^ <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= ((rng <*jt*>) \/ (rng <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= {jt} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A21: 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, A6, A9, A12, A10, A11, A20, A19, A22, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A20, A19, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A21, 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,v3} c= A holds
L is Convex_Combination of A
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def 6;
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

end;

suppose A23: 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 A24: F . 3 = v3 by FINSEQ_1:45;
A25: ( F . 1 = v2 & F . 2 = v1 ) by A23, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A24, FINSEQ_1:45;
then f = (<*jt*> ^ <*jt*>) ^ <*jt*> by FINSEQ_1:def 10;
then rng f = (rng (<*jt*> ^ <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= ((rng <*jt*>) \/ (rng <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= {jt} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A26: 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 A27: 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, A6, A9, A12, A10, A11, A25, A24, A27, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A25, A24, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A26, 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,v3} c= A holds
L is Convex_Combination of A
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def 6;
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

end;

suppose A28: 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 A29: F . 3 = v1 by FINSEQ_1:45;
A30: ( F . 1 = v2 & F . 2 = v3 ) by A28, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A29, FINSEQ_1:45;
then f = (<*jt*> ^ <*jt*>) ^ <*jt*> by FINSEQ_1:def 10;
then rng f = (rng (<*jt*> ^ <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= ((rng <*jt*>) \/ (rng <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= {jt} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A31: 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 A32: 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, A6, A9, A12, A10, A11, A30, A29, A32, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A30, A29, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A31, 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,v3} c= A holds
L is Convex_Combination of A
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def 6;
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

end;

suppose A33: 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 A34: F . 3 = v2 by FINSEQ_1:45;
A35: ( F . 1 = v3 & F . 2 = v1 ) by A33, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A34, FINSEQ_1:45;
then f = (<*jt*> ^ <*jt*>) ^ <*jt*> by FINSEQ_1:def 10;
then rng f = (rng (<*jt*> ^ <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= ((rng <*jt*>) \/ (rng <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= {jt} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A36: 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 A37: 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, A6, A9, A12, A10, A11, A35, A34, A37, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A35, A34, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A36, 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,v3} c= A holds
L is Convex_Combination of A
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def 6;
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

end;

suppose A38: 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 A39: F . 3 = v1 by FINSEQ_1:45;
A40: ( F . 1 = v3 & F . 2 = v2 ) by A38, FINSEQ_1:45;
then f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A39, FINSEQ_1:45;
then f = (<*jt*> ^ <*jt*>) ^ <*jt*> by FINSEQ_1:def 10;
then rng f = (rng (<*jt*> ^ <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= ((rng <*jt*>) \/ (rng <*jt*>)) \/ (rng <*jt*>) by FINSEQ_1:31
.= {jt} by FINSEQ_1:38 ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A41: 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 A42: 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, A6, A9, A12, A10, A11, A40, A39, A42, ENUMSET1:def 1, FINSEQ_3:1; :: thesis: verum

end;

f = <*(1 / 3),(1 / 3),(1 / 3)*> by A4, A6, A9, A12, A10, A11, A40, A39, FINSEQ_1:45;
then Sum f = ((1 / 3) + (1 / 3)) + (1 / 3) by RVSUM_1:78
.= 1 ;
then reconsider L = L as Convex_Combination of V by A5, A6, A41, 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,v3} c= A holds
L is Convex_Combination of A
for A being non empty Subset of V st {v1,v2,v3} c= A holds
L is Convex_Combination of A by A8, RLVECT_2:def 6;
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

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