let K be Field; :: thesis: for V being finite-dimensional VectSp of K
for B being OrdBasis of (Omega). V holds B is OrdBasis of V
let V be finite-dimensional VectSp of K; :: thesis: for B being OrdBasis of (Omega). V holds B is OrdBasis of V
let B be OrdBasis of (Omega). V; :: thesis: B is OrdBasis of V
reconsider r = rng B as Basis of (Omega). V by MATRLIN:def 4;
r is linearly-independent by VECTSP_7:def 3;
then reconsider R = r as linearly-independent Subset of V by VECTSP_9:15;
Lin R = Lin r by VECTSP_9:21
.= VectSpStr(# the carrier of V,the addF of V,the ZeroF of V,the lmult of V #) by VECTSP_7:def 3 ;
then A1: R is Basis of V by VECTSP_7:def 3;
B is one-to-one by MATRLIN:def 4;
hence B is OrdBasis of V by A1, MATRLIN:def 4; :: thesis: verum