let V be RealLinearSpace; :: thesis: for v1, v2 being VECTOR of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) )
let v1, v2 be VECTOR of V; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) )
thus ( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) ) ) :: thesis: ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )

proof

assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent ; :: thesis: ( v2 <> 0. V & ( for a being Real holds v1 <> a * v2 ) )
thus v2 <> 0. V by A2, Th11; :: thesis: for a being Real holds v1 <> a * v2
let a be Real; :: thesis: v1 <> a * v2
assume A3: v1 = a * v2 ; :: thesis: contradiction
deffunc H₁( Element of V) -> Element of NAT = 0 ;
consider f being Function of the carrier of V,REAL such that
A4: ( f . v1 = - 1 & f . v2 = a ) and
A5: for v being Element of V st v <> v1 & v <> v2 holds
f . v = H₁(v) from FUNCT_2:sch 7(A1);
reconsider f = f as Element of Funcs the carrier of V,REAL by FUNCT_2:11;

now

let v be VECTOR of V; :: thesis: ( not v in {v1,v2} implies f . v = 0 )
assume not v in {v1,v2} ; :: thesis: f . v = 0
then ( v <> v1 & v <> v2 ) by TARSKI:def 2;
hence f . v = 0 by A5; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v1,v2} )
assume x in Carrier f ; :: thesis: x in {v1,v2}
then A6: ex u being VECTOR of V st
( x = u & f . u <> 0 ) ;
assume not x in {v1,v2} ; :: thesis: contradiction
then ( x <> v1 & x <> v2 ) by TARSKI:def 2;
hence contradiction by A5, A6; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {v1,v2} by RLVECT_2:def 8;
A7: v1 in Carrier f by A4;
set w = a * v2;
Sum f = ((- 1) * (a * v2)) + (a * v2) by A1, A3, A4, RLVECT_2:51
.= (- (a * v2)) + (a * v2) by RLVECT_1:29
.= - ((a * v2) - (a * v2)) by RLVECT_1:47
.= - (0. V) by RLVECT_1:28
.= 0. V by RLVECT_1:25 ;
hence contradiction by A2, A7, Def1; :: thesis: verum

end;

assume A8: v2 <> 0. V ; :: thesis: ( ex a being Real st not v1 <> a * v2 or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A9: for a being Real holds v1 <> a * v2 ; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
then A10: ( v1 <> 1 * v2 & 1 * v2 = v2 ) by RLVECT_1:def 9;
hence v1 <> v2 ; :: thesis: {v1,v2} is linearly-independent
let l be Linear_Combination of {v1,v2}; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A11: Sum l = 0. V and
A12: Carrier l <> {} ; :: thesis: contradiction
consider x being Element of Carrier l;
x in Carrier l by A12;
then A13: ex u being VECTOR of V st
( x = u & l . u <> 0 ) ;
Carrier l c= {v1,v2} by RLVECT_2:def 8;
then A14: x in {v1,v2} by A12, TARSKI:def 3;
A15: 0. V = ((l . v1) * v1) + ((l . v2) * v2) by A10, A11, RLVECT_2:51;

now

per cases ( l . v1 <> 0 or ( l . v2 <> 0 & l . v1 = 0 ) ) by A13, A14, TARSKI:def 2;

suppose A16: l . v1 <> 0 ; :: thesis: contradiction

0. V = ((l . v1) " ) * (((l . v1) * v1) + ((l . v2) * v2)) by A15, RLVECT_1:23
.= (((l . v1) " ) * ((l . v1) * v1)) + (((l . v1) " ) * ((l . v2) * v2)) by RLVECT_1:def 9
.= ((((l . v1) " ) * (l . v1)) * v1) + (((l . v1) " ) * ((l . v2) * v2)) by RLVECT_1:def 9
.= ((((l . v1) " ) * (l . v1)) * v1) + ((((l . v1) " ) * (l . v2)) * v2) by RLVECT_1:def 9
.= (1 * v1) + ((((l . v1) " ) * (l . v2)) * v2) by A16, XCMPLX_0:def 7
.= v1 + ((((l . v1) " ) * (l . v2)) * v2) by RLVECT_1:def 9 ;
then v1 = - ((((l . v1) " ) * (l . v2)) * v2) by RLVECT_1:19
.= (- 1) * ((((l . v1) " ) * (l . v2)) * v2) by RLVECT_1:29
.= ((- 1) * (((l . v1) " ) * (l . v2))) * v2 by RLVECT_1:def 9 ;
hence contradiction by A9; :: thesis: verum

end;

suppose A17: ( l . v2 <> 0 & l . v1 = 0 ) ; :: thesis: contradiction

0. V = ((l . v2) " ) * (((l . v1) * v1) + ((l . v2) * v2)) by A15, RLVECT_1:23
.= (((l . v2) " ) * ((l . v1) * v1)) + (((l . v2) " ) * ((l . v2) * v2)) by RLVECT_1:def 9
.= ((((l . v2) " ) * (l . v1)) * v1) + (((l . v2) " ) * ((l . v2) * v2)) by RLVECT_1:def 9
.= ((((l . v2) " ) * (l . v1)) * v1) + ((((l . v2) " ) * (l . v2)) * v2) by RLVECT_1:def 9
.= ((((l . v2) " ) * (l . v1)) * v1) + (1 * v2) by A17, XCMPLX_0:def 7
.= (0 * v1) + v2 by A17, RLVECT_1:def 9
.= (0. V) + v2 by RLVECT_1:23
.= v2 by RLVECT_1:10 ;
hence contradiction by A8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum