:: deftheorem Def2 defines OrdBasis MATRLIN:def 2 :
for K being Field
for V being finite-dimensional VectSp of K
for b₃ being FinSequence of V holds
( b₃ is OrdBasis of V iff ( b₃ is one-to-one & rng b₃ is Basis of V ) );