let x be set ; :: thesis: for V being RealLinearSpace
for w1, w2 being VECTOR of V holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let V be RealLinearSpace; :: thesis: for w1, w2 being VECTOR of V holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let w1, w2 be VECTOR of V; :: thesis: ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
thus ( x in Lin {w1,w2} implies ex a, b being Real st x = (a * w1) + (b * w2) ) :: thesis: ( ex a, b being Real st x = (a * w1) + (b * w2) implies x in Lin {w1,w2} )

proof

assume A1: x in Lin {w1,w2} ; :: thesis: ex a, b being Real st x = (a * w1) + (b * w2)

now :: thesis: ex a, b being Real st x = (a * w1) + (b * w2)

per cases ( w1 = w2 or w1 <> w2 ) ;

suppose w1 = w2 ; :: thesis: ex a, b being Real st x = (a * w1) + (b * w2)

then {w1,w2} = {w1} by ENUMSET1:29;
then consider a being Real such that
A2: x = a * w1 by A1, Th8;
x = (a * w1) + (0. V) by A2, RLVECT_1:4
.= (a * w1) + (0 * w2) by RLVECT_1:10 ;
hence ex a, b being Real st x = (a * w1) + (b * w2) ; :: thesis: verum

end;

suppose A3: w1 <> w2 ; :: thesis: ex a, b being Real st x = (a * w1) + (b * w2)

consider l being Linear_Combination of {w1,w2} such that
A4: x = Sum l by A1, RLVECT_3:14;
x = ((l . w1) * w1) + ((l . w2) * w2) by A3, A4, RLVECT_2:33;
hence ex a, b being Real st x = (a * w1) + (b * w2) ; :: thesis: verum

end;

end;

end;

hence ex a, b being Real st x = (a * w1) + (b * w2) ; :: thesis: verum

end;

given a, b being Real such that A5: x = (a * w1) + (b * w2) ; :: thesis: x in Lin {w1,w2}

now :: thesis: x in Lin {w1,w2}

per cases ( w1 = w2 or w1 <> w2 ) ;

suppose A6: w1 = w2 ; :: thesis: x in Lin {w1,w2}

then x = (a + b) * w1 by A5, RLVECT_1:def 6;
then x in Lin {w1} by Th8;
hence x in Lin {w1,w2} by A6, ENUMSET1:29; :: thesis: verum

end;

suppose A7: w1 <> w2 ; :: thesis: x in Lin {w1,w2}

deffunc H₁( VECTOR of V) -> Element of REAL = zz;
reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V,REAL such that
A8: ( f . w1 = aa & f . w2 = bb ) and
A9: for u being VECTOR of V st u <> w1 & u <> w2 holds
f . u = H₁(u) from FUNCT_2:sch 7(A7);
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 {w1,w2} holds
f . u = 0

let u be VECTOR of V; :: thesis: ( not u in {w1,w2} implies f . u = 0 )
assume not u in {w1,w2} ; :: thesis: f . u = 0
then ( u <> w1 & u <> w2 ) by TARSKI:def 2;
hence f . u = 0 by A9; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;
Carrier f c= {w1,w2}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {w1,w2} )
assume that
A10: x in Carrier f and
A11: not x in {w1,w2} ; :: thesis: contradiction
( x <> w1 & x <> w2 ) by A11, TARSKI:def 2;
then f . x = 0 by A9, A10;
hence contradiction by A10, RLVECT_2:19; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def 6;
x = Sum f by A5, A7, A8, RLVECT_2:33;
hence x in Lin {w1,w2} by RLVECT_3:14; :: thesis: verum

end;

end;

end;

hence x in Lin {w1,w2} ; :: thesis: verum