:: deftheorem defOrdBasis defines OrdBasis ZMATRLIN:def 5 :
for V being free finite-rank Z_Module
for b₂ being FinSequence of V holds
( b₂ is OrdBasis of V iff ( b₂ is one-to-one & rng b₂ is Basis of V ) );