let V be torsion-free Z_Module; for v, u being Vector of V st v <> 0. V & u <> 0. V & (Lin {v}) /\ (Lin {u}) <> (0). V holds
rank ((Lin {v}) + (Lin {u})) = 1
let v, u be Vector of V; ( v <> 0. V & u <> 0. V & (Lin {v}) /\ (Lin {u}) <> (0). V implies rank ((Lin {v}) + (Lin {u})) = 1 )
assume A1:
( v <> 0. V & u <> 0. V & (Lin {v}) /\ (Lin {u}) <> (0). V )
; rank ((Lin {v}) + (Lin {u})) = 1
consider w being Vector of V such that
A2:
( w <> 0. V & (Lin {v}) + (Lin {u}) = Lin {w} )
by A1, LmSumMod2;
w in Lin {w}
by ZMODUL02:65, ZFMISC_1:31;
then reconsider ww = w as Vector of (Lin {w}) ;
A3:
ww <> 0. (Lin {w})
by A2, ZMODUL01:26;
(Omega). (Lin {w}) = Lin {ww}
by ZMODUL03:20;
hence
rank ((Lin {v}) + (Lin {u})) = 1
by A2, A3, ZMODUL05:5; verum