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
A3: [#] V is finite by A1;
reconsider C = [#] V as finite set by A1;
A4: card ([#] V) = card C ;
reconsider V = V as finite-dimensional VectSp of F by A3, Th4;
ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )

proof

consider x, y being set such that
A5: x <> y and
A6: [#] V = {x,y} by A1, A4, CARD_2:79;

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

suppose A7: x = 0. V ; :: thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )

reconsider y = y as Element of V by A6, TARSKI:def 2;
reconsider x = x as Element of V by A7;
set L = Lin {y};
A8: for v being Element of V holds
( v in (Omega). V iff v in Lin {y} )

proof

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} )

proof

assume v in (Omega). V ; :: thesis: v in Lin {y}
A9: y in {y} by TARSKI:def 1;
A10: 0. (Lin {y}) in Lin {y} by STRUCT_0:def 5;

per cases ( v = x or v = y ) by A6, TARSKI:def 2;

suppose v = x ; :: thesis: v in Lin {y}

hence v in Lin {y} by A7, A10, VECTSP_4:def 2; :: thesis: verum

end;

suppose v = y ; :: thesis: v in Lin {y}

hence v in Lin {y} by A9, VECTSP_7:13; :: thesis: verum

end;

end;

end;

hence ( v in (Omega). V iff v in Lin {y} ) by STRUCT_0:def 5; :: thesis: verum

end;

take y ; :: thesis: ( y <> 0. V & (Omega). V = Lin {y} )
thus ( y <> 0. V & (Omega). V = Lin {y} ) by A5, A7, A8, VECTSP_4:38; :: thesis: verum

end;

suppose A11: y = 0. V ; :: thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )

then reconsider y = y as Element of V ;
reconsider x = x as Element of V by A6, TARSKI:def 2;
set L = Lin {x};
A12: for v being Element of V holds
( v in (Omega). V iff v in Lin {x} )

proof

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} )

proof

assume v in (Omega). V ; :: thesis: v in Lin {x}
A13: x in {x} by TARSKI:def 1;
A14: 0. (Lin {x}) in Lin {x} by STRUCT_0:def 5;

per cases ( v = y or v = x ) by A6, TARSKI:def 2;

suppose v = y ; :: thesis: v in Lin {x}

hence v in Lin {x} by A11, A14, VECTSP_4:def 2; :: thesis: verum

end;

suppose v = x ; :: thesis: v in Lin {x}

hence v in Lin {x} by A13, VECTSP_7:13; :: thesis: verum

end;

end;

end;

hence ( v in (Omega). V iff v in Lin {x} ) by STRUCT_0:def 5; :: thesis: verum

end;

take x ; :: thesis: ( x <> 0. V & (Omega). V = Lin {x} )
thus ( x <> 0. V & (Omega). V = Lin {x} ) by A5, A11, A12, VECTSP_4:38; :: thesis: verum

end;

end;

end;

hence dim V = 1 by VECTSP_9:34; :: thesis: verum