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;
A3: card ([#] V) = card C ;
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

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

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

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

then reconsider x = x as Element of V ;
reconsider y = y as Element of V by A5, 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

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}
A7: y in {y} by TARSKI:def 1;
A8: 0. (Lin {y}) in Lin {y} by STRUCT_0:def 5;

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

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

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

end;

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

hence v in Lin {y} by A7, VECTSP_7:8; :: thesis: verum

end;

end;

end;

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

end;

hence ( y <> 0. V & (Omega). V = Lin {y} ) by A4, A6, VECTSP_4:30; :: thesis: verum

end;

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

reconsider x = x as Element of V by A5, TARSKI:def 2;
reconsider y = y as Element of V by A9;
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

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}
A10: x in {x} by TARSKI:def 1;
A11: 0. (Lin {x}) in Lin {x} by STRUCT_0:def 5;

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

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

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

end;

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

hence v in Lin {x} by A10, VECTSP_7:8; :: thesis: verum

end;

end;

end;

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

end;

hence ( x <> 0. V & (Omega). V = Lin {x} ) by A4, A9, VECTSP_4:30; :: thesis: verum

end;

end;

end;

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