let V be torsion-free Z_Module; :: thesis: for W being free finite-rank Submodule of V
for v being VECTOR of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
ex u being VECTOR of V st
( u <> 0. V & W /\ (Lin {v}) = Lin {u} )
let W be free finite-rank Submodule of V; :: thesis: for v being VECTOR of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
ex u being VECTOR of V st
( u <> 0. V & W /\ (Lin {v}) = Lin {u} )
let v be VECTOR of V; :: thesis: ( v <> 0. V & W /\ (Lin {v}) <> (0). V implies ex u being VECTOR of V st
( u <> 0. V & W /\ (Lin {v}) = Lin {u} ) )
assume A1: ( v <> 0. V & W /\ (Lin {v}) <> (0). V ) ; :: thesis: ex u being VECTOR of V st
( u <> 0. V & W /\ (Lin {v}) = Lin {u} )
rank (W /\ (Lin {v})) = 1 by A1, LmRank41;
then consider uu being VECTOR of (W /\ (Lin {v})) such that
A2: ( uu <> 0. (W /\ (Lin {v})) & (Omega). (W /\ (Lin {v})) = Lin {uu} ) by ZMODUL05:5;
reconsider u = uu as VECTOR of V by ZMODUL01:25;
A3: u <> 0. V by A2, ZMODUL01:26;
(Omega). (W /\ (Lin {v})) = Lin {u} by A2, ZMODUL03:20;
hence ex u being VECTOR of V st
( u <> 0. V & W /\ (Lin {v}) = Lin {u} ) by A3; :: thesis: verum