let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for a being Real st a <> 0 holds
ex l being Linear_Combination of V st
( l . v = a & Carrier l = {v} )
let v be VECTOR of V; :: thesis: for a being Real st a <> 0 holds
ex l being Linear_Combination of V st
( l . v = a & Carrier l = {v} )
let a be Real; :: thesis: ( a <> 0 implies ex l being Linear_Combination of V st
( l . v = a & Carrier l = {v} ) )
assume A1: a <> 0 ; :: thesis: ex l being Linear_Combination of V st
( l . v = a & Carrier l = {v} )
reconsider zz = 0 , a = a as Element of REAL by XREAL_0:def 1;
deffunc H₁( VECTOR of V) -> Element of REAL = zz;
consider f being Function of the carrier of V,REAL such that
A2: f . v = a and
A3: for u being VECTOR of V st u <> v holds
f . u = H₁(u) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

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

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in Carrier f )
assume x in {v} ; :: thesis: x in Carrier f
then x = v by TARSKI:def 1;
hence x in Carrier f by A1, A2; :: thesis: verum

end;

A6: 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 that
A7: x in Carrier f and
A8: not x in {v} ; :: thesis: contradiction
( f . x <> 0 & x <> v ) by A7, A8, RLVECT_2:19, TARSKI:def 1;
hence contradiction by A3, A7; :: thesis: verum

end;

take f ; :: thesis: ( f . v = a & Carrier f = {v} )
thus ( f . v = a & Carrier f = {v} ) by A2, A4, A6, XBOOLE_0:def 10; :: thesis: verum