let V be finite-dimensional RealUnitarySpace; :: thesis: ( dim V = 1 iff ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} ) )

( {v} is linearly-independent & Lin {v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) by A4, RLVECT_3:8, RUSUB_1:def 3;

then A5: {v} is Basis of V by RUSUB_3:def 2;

card {v} = 1 by CARD_1:30;

hence dim V = 1 by A5, Def2; :: thesis: verum

( v <> 0. V & (Omega). V = Lin {v} ) )

hereby :: thesis: ( ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} ) implies dim V = 1 )

given v being VECTOR of V such that A4:
( v <> 0. V & (Omega). V = Lin {v} )
; :: thesis: dim V = 1( v <> 0. V & (Omega). V = Lin {v} ) implies dim V = 1 )

consider I being finite Subset of V such that

A1: I is Basis of V by Def1;

assume dim V = 1 ; :: thesis: ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} )

then card I = 1 by A1, Def2;

then consider v being object such that

A2: I = {v} by CARD_2:42;

v in I by A2, TARSKI:def 1;

then reconsider v = v as VECTOR of V ;

{v} is linearly-independent by A1, A2, RUSUB_3:def 2;

then A3: v <> 0. V by RLVECT_3:8;

Lin {v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by A1, A2, RUSUB_3:def 2;

hence ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} ) by A3, RUSUB_1:def 3; :: thesis: verum

end;A1: I is Basis of V by Def1;

assume dim V = 1 ; :: thesis: ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} )

then card I = 1 by A1, Def2;

then consider v being object such that

A2: I = {v} by CARD_2:42;

v in I by A2, TARSKI:def 1;

then reconsider v = v as VECTOR of V ;

{v} is linearly-independent by A1, A2, RUSUB_3:def 2;

then A3: v <> 0. V by RLVECT_3:8;

Lin {v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by A1, A2, RUSUB_3:def 2;

hence ex v being VECTOR of V st

( v <> 0. V & (Omega). V = Lin {v} ) by A3, RUSUB_1:def 3; :: thesis: verum

( {v} is linearly-independent & Lin {v} = UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ) by A4, RLVECT_3:8, RUSUB_1:def 3;

then A5: {v} is Basis of V by RUSUB_3:def 2;

card {v} = 1 by CARD_1:30;

hence dim V = 1 by A5, Def2; :: thesis: verum