let x be object ; :: 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:29;
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:3;
x = (a * u) + (0. V) by A3, RLVECT_1:def 4
.= (a * u) + ((0. K) * v) by VECTSP10:1 ;
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 15;
hence x in Lin {u,v} by A2, VECTSP10:3; :: 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:7;
x = ((L . u) * u) + ((L . v) * v) by A5, A6, VECTSP_6:18;
hence ex a, b being Element of K st x = (a * u) + (b * v) ; :: thesis: verum

end;

deffunc H₁( set ) -> Element of the carrier of K = 0. K;
given a, b being Element of K such that A7: x = (a * u) + (b * v) ; :: thesis: x in Lin {u,v}
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:8;

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

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
A11: z <> u by A10, TARSKI:def 2;
z <> v by A10, TARSKI:def 2;
hence L . z = 0. K by A9, A11; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier L or x in {u,v} )
assume A12: x in Carrier L ; :: thesis: x in {u,v}
L . x <> 0. K by A12, VECTSP_6:2;
then ( x = v or x = u ) by A9, A12;
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 4;
Sum L = x by A5, A7, A8, VECTSP_6:18;
hence x in Lin {u,v} by VECTSP_7:7; :: thesis: verum

end;

end;