let n be Nat; :: thesis: for K being Field holds len (MX2FinS (1. (K,n))) = n
let K be Field; :: thesis: len (MX2FinS (1. (K,n))) = n
MX2FinS (1. (K,n)) is OrdBasis of n -VectSp_over K by MATRLIN2:45;
hence len (MX2FinS (1. (K,n))) = dim (n -VectSp_over K) by MATRLIN2:21
.= n by MATRIX13:112 ;
:: thesis: verum