let x be set ; :: thesis: for V being RealLinearSpace
for v being VECTOR of V holds
( x in Lin {v} iff ex a being Real st x = a * v )
let V be RealLinearSpace; :: thesis: for v being VECTOR of V holds
( x in Lin {v} iff ex a being Real st x = a * v )
let v be VECTOR of V; :: thesis: ( x in Lin {v} iff ex a being Real st x = a * v )
thus ( x in Lin {v} implies ex a being Real st x = a * v ) :: thesis: ( ex a being Real st x = a * v implies x in Lin {v} )

proof

assume x in Lin {v} ; :: thesis: ex a being Real st x = a * v
then consider l being Linear_Combination of {v} such that
A1: x = Sum l by RLVECT_3:14;
Sum l = (l . v) * v by RLVECT_2:32;
hence ex a being Real st x = a * v by A1; :: thesis: verum

end;

given a being Real such that A2: x = a * v ; :: thesis: x in Lin {v}
deffunc H₁( VECTOR of V) -> Element of REAL = zz;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V,REAL such that
A3: f . v = aa and
A4: for z being VECTOR of V st z <> v holds
f . z = H₁(z) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for z being VECTOR of V st not z in {v} holds
f . z = 0

let z be VECTOR of V; :: thesis: ( not z in {v} implies f . z = 0 )
assume not z in {v} ; :: thesis: f . z = 0
then z <> v by TARSKI:def 1;
hence f . z = 0 by A4; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {v}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )
assume A5: x in Carrier f ; :: thesis: x in {v}
then f . x <> 0 by RLVECT_2:19;
then x = v by A4, A5;
hence x in {v} by TARSKI:def 1; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def 6;
Sum f = x by A2, A3, RLVECT_2:32;
hence x in Lin {v} by RLVECT_3:14; :: thesis: verum