let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for L being Linear_Combination of V st L is convex & Carrier L = {v} holds

( L . v = 1 & Sum L = (L . v) * v )

let v be VECTOR of V; :: thesis: for L being Linear_Combination of V st L is convex & Carrier L = {v} holds

( L . v = 1 & Sum L = (L . v) * v )

let L be Linear_Combination of V; :: thesis: ( L is convex & Carrier L = {v} implies ( L . v = 1 & Sum L = (L . v) * v ) )

assume that

A1: L is convex and

A2: Carrier L = {v} ; :: thesis: ( L . v = 1 & Sum L = (L . v) * v )

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

consider F being FinSequence of the carrier of V such that

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

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

A5: F = <*v*> by A2, A3, FINSEQ_3:97;

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 A4;

reconsider r = f /. 1 as Element of REAL ;

card (Carrier L) = 1 by A2, CARD_1:30;

then len F = 1 by A3, FINSEQ_4:62;

then A9: dom f = Seg 1 by A6, FINSEQ_1:def 3;

then A10: 1 in dom f by FINSEQ_1:2, TARSKI:def 1;

then A11: f . 1 = f /. 1 by PARTFUN1:def 6;

then f = <*r*> by A9, FINSEQ_1:def 8;

then A12: Sum f = r by FINSOP_1:11;

f . 1 = L . (F . 1) by A8, A10;

hence ( L . v = 1 & Sum L = (L . v) * v ) by A7, A11, A12, A5, FINSEQ_1:def 8, RLVECT_2:32; :: thesis: verum

for L being Linear_Combination of V st L is convex & Carrier L = {v} holds

( L . v = 1 & Sum L = (L . v) * v )

let v be VECTOR of V; :: thesis: for L being Linear_Combination of V st L is convex & Carrier L = {v} holds

( L . v = 1 & Sum L = (L . v) * v )

let L be Linear_Combination of V; :: thesis: ( L is convex & Carrier L = {v} implies ( L . v = 1 & Sum L = (L . v) * v ) )

assume that

A1: L is convex and

A2: Carrier L = {v} ; :: thesis: ( L . v = 1 & Sum L = (L . v) * v )

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

consider F being FinSequence of the carrier of V such that

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

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

A5: F = <*v*> by A2, A3, FINSEQ_3:97;

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 A4;

reconsider r = f /. 1 as Element of REAL ;

card (Carrier L) = 1 by A2, CARD_1:30;

then len F = 1 by A3, FINSEQ_4:62;

then A9: dom f = Seg 1 by A6, FINSEQ_1:def 3;

then A10: 1 in dom f by FINSEQ_1:2, TARSKI:def 1;

then A11: f . 1 = f /. 1 by PARTFUN1:def 6;

then f = <*r*> by A9, FINSEQ_1:def 8;

then A12: Sum f = r by FINSOP_1:11;

f . 1 = L . (F . 1) by A8, A10;

hence ( L . v = 1 & Sum L = (L . v) * v ) by A7, A11, A12, A5, FINSEQ_1:def 8, RLVECT_2:32; :: thesis: verum