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 12;
then 1. K,n is diagonal by MATRIX_1:def 15;
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 4; :: thesis: verum