theorem LmSumMod3: :: ZMODUL06:29

for V being torsion-free Z_Module
for W being free finite-rank Subspace of V
for v, u being Vector of V st v <> 0. V & u <> 0. V & W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V & (Lin {u}) /\ (Lin {v}) = (0). V holds
ex w1, w2 being Vector of V st
( w1 <> 0. V & w2 <> 0. V & (W + (Lin {u})) + (Lin {v}) = (W + (Lin {w1})) + (Lin {w2}) & W /\ (Lin {w1}) <> (0). V & (W + (Lin {w1})) /\ (Lin {w2}) = (0). V & u in (Lin {w1}) + (Lin {w2}) & v in (Lin {w1}) + (Lin {w2}) & w1 in (Lin {u}) + (Lin {v}) & w2 in (Lin {u}) + (Lin {v}) )