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 2;
r is linearly-independent by VECTSP_7:def 3;
then reconsider R = r as linearly-independent Subset of V by VECTSP_9:11;
Lin R = Lin r by VECTSP_9:17
.= ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by VECTSP_7:def 3 ;
then R is Basis of V by VECTSP_7:def 3;
hence B is OrdBasis of V by MATRLIN:def 2; :: thesis: verum