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

proof

consider x, y being object such that
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;

suppose A5: 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 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

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

end;

suppose A8: 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 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} )

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

end;

end;

end;

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