theorem Th21: :: MATRLIN2:21

for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds len b1 = dim V1