let V be torsion-free Z_Module; :: thesis: for v being Vector of V st v <> 0. V holds
rank (Lin {v}) = 1
let v be Vector of V; :: thesis: ( v <> 0. V implies rank (Lin {v}) = 1 )
assume A1: v <> 0. V ; :: thesis: rank (Lin {v}) = 1
v in Lin {v} by ZMODUL02:65, ZFMISC_1:31;
then reconsider vv = v as Vector of (Lin {v}) ;
A2: vv <> 0. (Lin {v}) by A1, ZMODUL01:26;
(Omega). (Lin {v}) = Lin {vv} by ZMODUL03:20;
hence rank (Lin {v}) = 1 by A2, ZMODUL05:5; :: thesis: verum