let V be free finite-rank Z_Module; :: thesis: ( rank V = 1 iff ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) )

hereby :: thesis: ( ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) implies rank V = 1 )

consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
assume rank V = 1 ; :: thesis: ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} )
then card I = 1 by A1, ZMODUL03:def 5;
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 ;
A3: v <> 0. V by A1, A2, VECTSP_7:def 3;
Lin {v} = ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by A1, A2, VECTSP_7:def 3;
hence ex v being VECTOR of V st
( v <> 0. V & (Omega). V = Lin {v} ) by A3; :: thesis: verum

end;

given v being VECTOR of V such that A4: ( v <> 0. V & (Omega). V = Lin {v} ) ; :: thesis: rank V = 1
( {v} is linearly-independent & Lin {v} = ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) by A4, ZMODUL02:59;
then A5: {v} is Basis of V by VECTSP_7:def 3;
card {v} = 1 by CARD_1:30;
hence rank V = 1 by A5, ZMODUL03:def 5; :: thesis: verum