theorem Th45: :: MATRLIN2:45

for n being Nat
for K being Field holds MX2FinS (1. (K,n)) is OrdBasis of n -VectSp_over K