for K being Field
for V2 being finite-dimensional VectSp of K
for b2 being OrdBasis of V2
for v1, v2 being Vector of V2 st v1 |-- b2 = v2 |-- b2 holds
v1 = v2