theorem Th20: :: MATRLIN2:20

for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds (0. V1) |-- b1 = (len b1) |-> (0. K)