let F be Field; :: thesis: for V being VectSp of F st card ([#] V) = 2 holds

dim V = 1

let V be VectSp of F; :: thesis: ( card ([#] V) = 2 implies dim V = 1 )

assume A1: card ([#] V) = 2 ; :: thesis: dim V = 1

then A2: [#] V is finite ;

reconsider C = [#] V as finite set by A1;

reconsider V = V as finite-dimensional VectSp of F by A2, Th4;

ex v being Vector of V st

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

dim V = 1

let V be VectSp of F; :: thesis: ( card ([#] V) = 2 implies dim V = 1 )

assume A1: card ([#] V) = 2 ; :: thesis: dim V = 1

then A2: [#] V is finite ;

reconsider C = [#] V as finite set by A1;

reconsider V = V as finite-dimensional VectSp of F by A2, Th4;

ex v being Vector of V st

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

proof

hence
dim V = 1
by VECTSP_9:30; :: thesis: verum
consider x, y being object such that

A3: x <> y and

A4: [#] V = {x,y} by A1, CARD_2:60;

end;A3: x <> y and

A4: [#] V = {x,y} by A1, CARD_2:60;

per cases
( x = 0. V or y = 0. V )
by A4, TARSKI:def 2;

end;

suppose A5:
x = 0. V
; :: thesis: ex v being Vector of V st

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

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

then reconsider x = x as Element of V ;

reconsider y = y as Element of V by A4, TARSKI:def 2;

set L = Lin {y};

take y ; :: thesis: ( y <> 0. V & (Omega). V = Lin {y} )

for v being Element of V holds

( v in (Omega). V iff v in Lin {y} )

end;reconsider y = y as Element of V by A4, TARSKI:def 2;

set L = Lin {y};

take y ; :: thesis: ( y <> 0. V & (Omega). V = Lin {y} )

for v being Element of V holds

( v in (Omega). V iff v in Lin {y} )

proof

hence
( y <> 0. V & (Omega). V = Lin {y} )
by A3, A5, VECTSP_4:30; :: thesis: verum
let v be Element of V; :: thesis: ( v in (Omega). V iff v in Lin {y} )

( v in (Omega). V implies v in Lin {y} )

end;( v in (Omega). V implies v in Lin {y} )

proof

hence
( v in (Omega). V iff v in Lin {y} )
; :: thesis: verum
assume
v in (Omega). V
; :: thesis: v in Lin {y}

A6: y in {y} by TARSKI:def 1;

A7: 0. (Lin {y}) in Lin {y} ;

end;A6: y in {y} by TARSKI:def 1;

A7: 0. (Lin {y}) in Lin {y} ;

suppose A8:
y = 0. V
; :: thesis: ex v being Vector of V st

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

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

reconsider x = x as Element of V by A4, TARSKI:def 2;

reconsider y = y as Element of V by A8;

set L = Lin {x};

take x ; :: thesis: ( x <> 0. V & (Omega). V = Lin {x} )

for v being Element of V holds

( v in (Omega). V iff v in Lin {x} )

end;reconsider y = y as Element of V by A8;

set L = Lin {x};

take x ; :: thesis: ( x <> 0. V & (Omega). V = Lin {x} )

for v being Element of V holds

( v in (Omega). V iff v in Lin {x} )

proof

hence
( x <> 0. V & (Omega). V = Lin {x} )
by A3, A8, VECTSP_4:30; :: thesis: verum
let v be Element of V; :: thesis: ( v in (Omega). V iff v in Lin {x} )

( v in (Omega). V implies v in Lin {x} )

end;( v in (Omega). V implies v in Lin {x} )

proof

hence
( v in (Omega). V iff v in Lin {x} )
; :: thesis: verum
assume
v in (Omega). V
; :: thesis: v in Lin {x}

A9: x in {x} by TARSKI:def 1;

A10: 0. (Lin {x}) in Lin {x} ;

end;A9: x in {x} by TARSKI:def 1;

A10: 0. (Lin {x}) in Lin {x} ;