let x be set ; :: thesis: for K being Field
for V being VectSp of K
for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
let K be Field; :: thesis: for V being VectSp of K
for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
let V be VectSp of K; :: thesis: for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )
let u, v be Vector of V; :: thesis: ( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )

per cases ( u = v or u <> v ) ;

suppose A1: u = v ; :: thesis: ( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )

then A2: {u,v} = {u} by ENUMSET1:69;
thus ( x in Lin {u,v} implies ex a, b being Element of K st x = (a * u) + (b * v) ) :: thesis: ( ex a, b being Element of K st x = (a * u) + (b * v) implies x in Lin {u,v} )

proof

assume x in Lin {u,v} ; :: thesis: ex a, b being Element of K st x = (a * u) + (b * v)
then consider a being Element of K such that
A3: x = a * u by A2, VECTSP10:4;
x = (a * u) + (0. V) by A3, RLVECT_1:def 7
.= (a * u) + ((0. K) * v) by VECTSP10:2 ;
hence ex a, b being Element of K st x = (a * u) + (b * v) ; :: thesis: verum

end;

given a, b being Element of K such that A4: x = (a * u) + (b * v) ; :: thesis: x in Lin {u,v}
x = (a + b) * u by A1, A4, VECTSP_1:def 26;
hence x in Lin {u,v} by A2, VECTSP10:4; :: thesis: verum

end;

suppose A5: u <> v ; :: thesis: ( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )

thus ( x in Lin {u,v} implies ex a, b being Element of K st x = (a * u) + (b * v) ) :: thesis: ( ex a, b being Element of K st x = (a * u) + (b * v) implies x in Lin {u,v} )

proof

assume x in Lin {u,v} ; :: thesis: ex a, b being Element of K st x = (a * u) + (b * v)
then consider L being Linear_Combination of {u,v} such that
A6: x = Sum L by VECTSP_7:12;
x = ((L . u) * u) + ((L . v) * v) by A5, A6, VECTSP_6:44;
hence ex a, b being Element of K st x = (a * u) + (b * v) ; :: thesis: verum

end;

given a, b being Element of K such that A7: x = (a * u) + (b * v) ; :: thesis: x in Lin {u,v}
deffunc H₁( set ) -> Element of the carrier of K = 0. K;
consider L being Function of the carrier of V,the carrier of K such that
A8: ( L . u = a & L . v = b ) and
A9: for z being Element of V st z <> u & z <> v holds
L . z = H₁(z) from FUNCT_2:sch 7(A5);
reconsider L = L as Element of Funcs the carrier of V,the carrier of K by FUNCT_2:11;

now

let z be Vector of V; :: thesis: ( not z in {u,v} implies L . z = 0. K )
assume A10: not z in {u,v} ; :: thesis: L . z = 0. K
( z <> v & z <> u ) by A10, TARSKI:def 2;
hence L . z = 0. K by A9; :: thesis: verum

end;

then reconsider L = L as Linear_Combination of V by VECTSP_6:def 4;
Carrier L c= {u,v}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier L or x in {u,v} )
assume A11: x in Carrier L ; :: thesis: x in {u,v}
L . x <> 0. K by A11, VECTSP_6:20;
then ( x = v or x = u ) by A9, A11;
hence x in {u,v} by TARSKI:def 2; :: thesis: verum

end;

then reconsider L = L as Linear_Combination of {u,v} by VECTSP_6:def 7;
Sum L = x by A5, A7, A8, VECTSP_6:44;
hence x in Lin {u,v} by VECTSP_7:12; :: thesis: verum

end;

end;