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} )

deffunc H_{1}( 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_{1}(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;

Carrier f c= {v}

Sum f = x by A2, A3, VECTSP_6:17;

hence x in Lin {v} by VECTSP_7:7; :: thesis: verum

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

given a being Element of K such that A2:
x = a * v
; :: thesis: x in Lin {v}
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;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

deffunc H

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

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

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;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;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

Carrier f c= {v}

proof

then reconsider f = f as Linear_Combination of {v} by VECTSP_6:def 4;
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;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

Sum f = x by A2, A3, VECTSP_6:17;

hence x in Lin {v} by VECTSP_7:7; :: thesis: verum