for V being free finite-rank Z_Module
for A, B being Basis of V holds card A = card B