theorem :: ZMODUL04:32

for V being free Z_Module
for I being Basis of V
for v being Vector of V st v in I holds
( Lin (I \ {v}) is free & Lin {v} is free )