theorem :: MATRLIN2:4

for K being Field
for V being finite-dimensional VectSp of K
for B being OrdBasis of (Omega). V holds B is OrdBasis of V