let V be RealLinearSpace; :: thesis: for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let v1, v2 be VECTOR of V; :: thesis: for L being Linear_Combination of V st L is circled & Carrier L = {v1,v2} & v1 <> v2 holds
( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let L be Linear_Combination of V; :: thesis: ( L is circled & Carrier L = {v1,v2} & v1 <> v2 implies ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) )
assume that
A1: L is circled and
A2: Carrier L = {v1,v2} and
A3: v1 <> v2 ; :: thesis: ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
reconsider L = L as Linear_Combination of {v1,v2} by A2, RLVECT_2:def 8;
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, Def4;
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} by A2, A4, FINSEQ_4:77;
then A6: len f = 2 by A3, A5, CARD_2:76;
then dom f = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
then A7: ( 1 in dom f & 2 in dom f ) by TARSKI:def 2;
then A8: ( f . 1 = L . (F . 1) & f . 1 >= 0 ) by A5;
then ( f /. 1 = L . (F . 1) & L . (F . 1) >= 0 ) 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) & L . (F . 2) >= 0 ) by A7, PARTFUN1:def 8;
then reconsider r2 = L . (F . 2) as Element of REAL ;
A10: f = <*r1,r2*> by A6, A8, A9, FINSEQ_1:61;

now

per cases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A2, A3, A4, FINSEQ_3:108;

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

then ( F . 1 = v1 & F . 2 = v2 ) by FINSEQ_1:61;
hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A5, A8, A9, A10, RVSUM_1:107; :: thesis: verum

end;

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

then ( F . 1 = v2 & F . 2 = v1 ) by FINSEQ_1:61;
hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 ) by A5, A8, A9, A10, RVSUM_1:107; :: thesis: verum

end;

end;

end;

hence ( (L . v1) + (L . v2) = 1 & L . v1 >= 0 & L . v2 >= 0 & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A3, RLVECT_2:51; :: thesis: verum