let V be RealUnitarySpace; :: thesis: for w1, w2 being VECTOR of V
for x being set 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: for x being set holds
( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )
let x be set ; :: 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

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:69;
then consider a being Real such that
A2: x = a * w1 by A1, Th29;
x = (a * w1) + (0. V) by A2, RLVECT_1:10
.= (a * w1) + (0 * w2) by RLVECT_1:23 ;
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, Th1;
x = ((l . w1) * w1) + ((l . w2) * w2) by A3, A4, RLVECT_2:51;
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

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 9;
then x in Lin {w1} by Th29;
hence x in Lin {w1,w2} by A6, ENUMSET1:69; :: thesis: verum

end;

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

deffunc H₁( set ) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A8: f . w1 = a and
A9: f . w2 = b and
A10: 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:11;

now

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 A10; :: thesis: verum

end;

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

proof

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

end;

then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def 8;
x = Sum f by A5, A7, A8, A9, RLVECT_2:51;
hence x in Lin {w1,w2} by Th1; :: thesis: verum

end;

end;

end;

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