theorem Th19: :: MATRLIN2:19

for i being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 st i in dom b1 holds
(b1 /. i) |-- b1 = Line ((1. (K,(len b1))),i)