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

for L being Linear_Combination of {v} st L is convex 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 holds

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

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

Carrier L c= {v} by RLVECT_2:def 6;

then A1: ( Carrier L = {} or Carrier L = {v} ) by ZFMISC_1:33;

assume L is convex ; :: thesis: ( L . v = 1 & Sum L = (L . v) * v )

hence ( L . v = 1 & Sum L = (L . v) * v ) by A1, Lm11, Th21; :: thesis: verum

for L being Linear_Combination of {v} st L is convex 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 holds

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

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

Carrier L c= {v} by RLVECT_2:def 6;

then A1: ( Carrier L = {} or Carrier L = {v} ) by ZFMISC_1:33;

assume L is convex ; :: thesis: ( L . v = 1 & Sum L = (L . v) * v )

hence ( L . v = 1 & Sum L = (L . v) * v ) by A1, Lm11, Th21; :: thesis: verum