let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for L being Linear_Combination of {v} st L is circled 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 circled holds
( L . v = 1 & Sum L = (L . v) * v )
let L be Linear_Combination of {v}; :: thesis: ( L is circled 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 circled ; :: thesis: ( L . v = 1 & Sum L = (L . v) * v )
hence ( L . v = 1 & Sum L = (L . v) * v ) by A1, Th16, Th22; :: thesis: verum