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