theorem Th46: :: MATRLIN2:46

for K being Field
for V2 being finite-dimensional VectSp of K
for b2 being OrdBasis of V2
for M being OrdBasis of (len b2) -VectSp_over K st M = MX2FinS (1. (K,(len b2))) holds
for v1 being Vector of ((len b2) -VectSp_over K) holds v1 |-- M = v1