let V be ComplexLinearSpace; :: thesis: for v1, v2, v3 being VECTOR of V
for L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds
( ex r1, r2, r3 being real number st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
let v1, v2, v3 be VECTOR of V; :: thesis: for L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds
( ex r1, r2, r3 being real number st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
let L be C_Linear_Combination of V; :: thesis: ( L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 implies ( ex r1, r2, r3 being real number st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) )
assume that
A1: L is convex and
A2: Carrier L = {v1,v2,v3} and
A3: ( v1 <> v2 & v2 <> v3 & v3 <> v1 ) ; :: thesis: ( ex r1, r2, r3 being real number st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
reconsider L = L as C_Linear_Combination of {v1,v2,v3} by A2, Def3;
consider F being FinSequence of the carrier of V such that
A4: ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) ) by A1, Def203;
consider f being FinSequence of REAL such that
A5: ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A4;
len F = card {v1,v2,v3} by A2, A4, FINSEQ_4:77;
then A6: len f = 3 by A3, A5, CARD_2:77;
then dom f = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;
then A7: ( 1 in dom f & 2 in dom f & 3 in dom f ) by ENUMSET1:def 1;
then A8: ( f . 1 = L . (F . 1) & f . 1 >= 0 ) by A5;
then f /. 1 = L . (F . 1) by A7, PARTFUN1:def 8;
then reconsider r1 = L . (F . 1) as Element of REAL ;
A9: ( f . 2 = L . (F . 2) & f . 2 >= 0 ) by A5, A7;
then f /. 2 = L . (F . 2) by A7, PARTFUN1:def 8;
then reconsider r2 = L . (F . 2) as Element of REAL ;
A10: ( f . 3 = L . (F . 3) & f . 3 >= 0 ) by A5, A7;
then f /. 3 = L . (F . 3) by A7, PARTFUN1:def 8;
then reconsider r3 = L . (F . 3) as Element of REAL ;
B1: f = <*r1,r2,r3*> by A6, A8, A9, A10, FINSEQ_1:62;
then A11: (r1 + r2) + r3 = 1 by A5, RVSUM_1:108;
ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )

proof

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 A2, A3, A4, CONVEX1:31;

suppose F = <*v1,v2,v3*> ; :: thesis: ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )

then ( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) by B1, A5, A8, A9, A10, FINSEQ_1:62, RVSUM_1:108;
hence ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 ) ; :: thesis: verum

end;

suppose F = <*v1,v3,v2*> ; :: thesis: ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )

then ( r1 = L . v1 & r3 = L . v2 & r2 = L . v3 & (r1 + r3) + r2 = 1 & r1 >= 0 & r3 >= 0 & r2 >= 0 ) by A8, A9, A10, A11, FINSEQ_1:62;
hence ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 ) ; :: thesis: verum

end;

suppose F = <*v2,v1,v3*> ; :: thesis: ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )

then ( r2 = L . v1 & r1 = L . v2 & r3 = L . v3 & (r2 + r1) + r3 = 1 & r2 >= 0 & r1 >= 0 & r3 >= 0 ) by B1, A5, A8, A9, A10, FINSEQ_1:62, RVSUM_1:108;
hence ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 ) ; :: thesis: verum

end;

suppose F = <*v2,v3,v1*> ; :: thesis: ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )

then ( r3 = L . v1 & r1 = L . v2 & r2 = L . v3 & (r3 + r1) + r2 = 1 & r3 >= 0 & r1 >= 0 & r2 >= 0 ) by A8, A9, A10, A11, FINSEQ_1:62;
hence ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 ) ; :: thesis: verum

end;

suppose F = <*v3,v1,v2*> ; :: thesis: ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )

then ( r2 = L . v1 & r3 = L . v2 & r1 = L . v3 & (r2 + r3) + r1 = 1 & r2 >= 0 & r3 >= 0 & r1 >= 0 ) by A8, A9, A10, A11, FINSEQ_1:62;
hence ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 ) ; :: thesis: verum

end;

suppose F = <*v3,v2,v1*> ; :: thesis: ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )

then ( r3 = L . v1 & r2 = L . v2 & r1 = L . v3 & (r3 + r2) + r1 = 1 & r3 >= 0 & r2 >= 0 & r1 >= 0 ) by A8, A9, A10, A11, FINSEQ_1:62;
hence ex a, b, c being real number st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 ) ; :: thesis: verum

end;

end;

end;

hence ( ex r1, r2, r3 being real number st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) by A3, Lm214; :: thesis: verum