for V being free finite-rank Z_Module
for I being Basis of V ex J being OrdBasis of V st rng J = I