for V being Z_Module
for I being finite Subset of V
for W being Submodule of V st ( for v being VECTOR of V st v in I holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & a * v in W ) ) holds
ex a being Element of INT.Ring st
( a <> 0. INT.Ring & ( for v being VECTOR of V st v in I holds
a * v in W ) )