let K be Field; :: thesis: for V being VectSp of K
for x being object
for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
let V be VectSp of K; :: thesis: for x being object
for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
let x be object ; :: thesis: for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
let v be Vector of V; :: thesis: ( x in Lin {v} iff ex a being Element of K st x = a * v )
thus ( x in Lin {v} implies ex a being Element of K st x = a * v ) :: thesis: ( ex a being Element of K st x = a * v implies x in Lin {v} )

proof

assume x in Lin {v} ; :: thesis: ex a being Element of K st x = a * v
then consider l being Linear_Combination of {v} such that
A1: x = Sum l by VECTSP_7:7;
Sum l = (l . v) * v by VECTSP_6:17;
hence ex a being Element of K st x = a * v by A1; :: thesis: verum

end;

given a being Element of K such that A2: x = a * v ; :: thesis: x in Lin {v}
deffunc H₁( set ) -> Element of the carrier of K = 0. K;
consider f being Function of the carrier of V, the carrier of K such that
A3: f . v = a 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, the carrier of K) by FUNCT_2:8;

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

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

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
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. K by VECTSP_6:2;
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 VECTSP_6:def 4;
Sum f = x by A2, A3, VECTSP_6:17;
hence x in Lin {v} by VECTSP_7:7; :: thesis: verum