for V being free Z_Module
for I being Basis of V
for v being Vector of V holds v in Lin I