for V2 being free finite-rank Z_Module
for b2 being OrdBasis of V2
for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds
v1 = v2