let n be Nat; :: thesis: for K being Field holds MX2FinS (1. (K,n)) is OrdBasis of n -VectSp_over K
let K be Field; :: thesis: MX2FinS (1. (K,n)) is OrdBasis of n -VectSp_over K
set ONE = 1. (K,n);
A1: the_rank_of (1. (K,n)) = n by Lm6;
then A2: 1. (K,n) is one-to-one by MATRIX13:105;
for i, j being Nat st [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K holds
i = j by MATRIX_1:def 3;
then 1. (K,n) is diagonal by MATRIX_1:def 6;
then lines (1. (K,n)) is Basis of (n -VectSp_over K) by A1, MATRIX13:111;
hence MX2FinS (1. (K,n)) is OrdBasis of n -VectSp_over K by A2, MATRLIN:def 2; :: thesis: verum