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 U2 of V,the lmult of V #) by VECTSP_7:def 3 ;
then ( R is Basis of V & B is one-to-one ) by MATRLIN:def 4, VECTSP_7:def 3;
hence B is OrdBasis of V by MATRLIN:def 4; :: thesis: verum