let V be RealLinearSpace; :: thesis: for v1, v2, v3 being VECTOR of V

for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds

( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )

let v1, v2, v3 be VECTOR of V; :: thesis: for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds

( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )

let L be Linear_Combination of V; :: thesis: ( L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 implies ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 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: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )

reconsider L = L as Linear_Combination of {v1,v2,v3} by A2, RLVECT_2:def 6;

consider F being FinSequence of the carrier of V such that

A4: ( F is one-to-one & rng F = Carrier L ) and

A5: 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;

consider f being FinSequence of REAL such that

A6: len f = len F and

A7: Sum f = 1 and

A8: for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) by A5;

len F = card {v1,v2,v3} by A2, A4, FINSEQ_4:62;

then A9: len f = 3 by A3, A6, CARD_2:58;

then A10: dom f = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;

then A11: 1 in dom f by ENUMSET1:def 1;

then A12: f . 1 = L . (F . 1) by A8;

then f /. 1 = L . (F . 1) by A11, PARTFUN1:def 6;

then reconsider r1 = L . (F . 1) as Element of REAL ;

A13: 3 in dom f by A10, ENUMSET1:def 1;

then A14: f . 3 = L . (F . 3) by A8;

then f /. 3 = L . (F . 3) by A13, PARTFUN1:def 6;

then reconsider r3 = L . (F . 3) as Element of REAL ;

A15: 2 in dom f by A10, ENUMSET1:def 1;

then A16: f . 2 = L . (F . 2) by A8;

then f /. 2 = L . (F . 2) by A15, PARTFUN1:def 6;

then reconsider r2 = L . (F . 2) as Element of REAL ;

A17: f = <*r1,r2,r3*> by A9, A12, A16, A14, FINSEQ_1:45;

then A18: ((L . (F . 1)) + (L . (F . 2))) + (L . (F . 3)) = 1 by A7, RVSUM_1:78;

for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds

( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )

let v1, v2, v3 be VECTOR of V; :: thesis: for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds

( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )

let L be Linear_Combination of V; :: thesis: ( L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 implies ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 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: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )

reconsider L = L as Linear_Combination of {v1,v2,v3} by A2, RLVECT_2:def 6;

consider F being FinSequence of the carrier of V such that

A4: ( F is one-to-one & rng F = Carrier L ) and

A5: 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;

consider f being FinSequence of REAL such that

A6: len f = len F and

A7: Sum f = 1 and

A8: for n being Nat st n in dom f holds

( f . n = L . (F . n) & f . n >= 0 ) by A5;

len F = card {v1,v2,v3} by A2, A4, FINSEQ_4:62;

then A9: len f = 3 by A3, A6, CARD_2:58;

then A10: dom f = {1,2,3} by FINSEQ_1:def 3, FINSEQ_3:1;

then A11: 1 in dom f by ENUMSET1:def 1;

then A12: f . 1 = L . (F . 1) by A8;

then f /. 1 = L . (F . 1) by A11, PARTFUN1:def 6;

then reconsider r1 = L . (F . 1) as Element of REAL ;

A13: 3 in dom f by A10, ENUMSET1:def 1;

then A14: f . 3 = L . (F . 3) by A8;

then f /. 3 = L . (F . 3) by A13, PARTFUN1:def 6;

then reconsider r3 = L . (F . 3) as Element of REAL ;

A15: 2 in dom f by A10, ENUMSET1:def 1;

then A16: f . 2 = L . (F . 2) by A8;

then f /. 2 = L . (F . 2) by A15, PARTFUN1:def 6;

then reconsider r2 = L . (F . 2) as Element of REAL ;

A17: f = <*r1,r2,r3*> by A9, A12, A16, A14, FINSEQ_1:45;

then A18: ((L . (F . 1)) + (L . (F . 2))) + (L . (F . 3)) = 1 by A7, RVSUM_1:78;

now :: thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )end;

hence
( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
by A3, Lm14; :: thesis: verumper 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, Lm13;

end;

suppose A19:
F = <*v1,v2,v3*>
; :: thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )

then A20:
F . 3 = v3
by FINSEQ_1:45;

( F . 1 = v1 & F . 2 = v2 ) by A19, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A7, A8, A11, A15, A13, A12, A16, A14, A17, A20, RVSUM_1:78; :: thesis: verum

end;( F . 1 = v1 & F . 2 = v2 ) by A19, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A7, A8, A11, A15, A13, A12, A16, A14, A17, A20, RVSUM_1:78; :: thesis: verum

suppose A21:
F = <*v1,v3,v2*>
; :: thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )

then A22:
F . 3 = v2
by FINSEQ_1:45;

( F . 1 = v1 & F . 2 = v3 ) by A21, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A22; :: thesis: verum

end;( F . 1 = v1 & F . 2 = v3 ) by A21, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A22; :: thesis: verum

suppose A23:
F = <*v2,v1,v3*>
; :: thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )

then A24:
F . 3 = v3
by FINSEQ_1:45;

( F . 1 = v2 & F . 2 = v1 ) by A23, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A7, A8, A11, A15, A13, A12, A16, A14, A17, A24, RVSUM_1:78; :: thesis: verum

end;( F . 1 = v2 & F . 2 = v1 ) by A23, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A7, A8, A11, A15, A13, A12, A16, A14, A17, A24, RVSUM_1:78; :: thesis: verum

suppose A25:
F = <*v2,v3,v1*>
; :: thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )

then A26:
F . 3 = v1
by FINSEQ_1:45;

( F . 1 = v2 & F . 2 = v3 ) by A25, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A26; :: thesis: verum

end;( F . 1 = v2 & F . 2 = v3 ) by A25, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A26; :: thesis: verum

suppose A27:
F = <*v3,v1,v2*>
; :: thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )

then A28:
F . 3 = v2
by FINSEQ_1:45;

( F . 1 = v3 & F . 2 = v1 ) by A27, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A28; :: thesis: verum

end;( F . 1 = v3 & F . 2 = v1 ) by A27, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A28; :: thesis: verum

suppose A29:
F = <*v3,v2,v1*>
; :: thesis: ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 )

then A30:
F . 3 = v1
by FINSEQ_1:45;

( F . 1 = v3 & F . 2 = v2 ) by A29, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A30; :: thesis: verum

end;( F . 1 = v3 & F . 2 = v2 ) by A29, FINSEQ_1:45;

hence ( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 ) by A8, A11, A15, A13, A12, A16, A14, A18, A30; :: thesis: verum