let V be torsion-free Z_Module; :: thesis: for W being free finite-rank Subspace 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 Subspace 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