theorem LmSumMod2: :: ZMODUL06:28

for V being torsion-free Z_Module
for v1, v2 being Vector of V st v1 <> 0. V & v2 <> 0. V & (Lin {v1}) /\ (Lin {v2}) <> (0). V holds
ex u being Vector of V st
( u <> 0. V & (Lin {v1}) + (Lin {v2}) = Lin {u} )