let n be Nat; :: thesis: for K being Field holds
( lines (1. (K,n)) is Basis of (n -VectSp_over K) & the_rank_of (1. (K,n)) = n )
let K be Field; :: thesis: ( lines (1. (K,n)) is Basis of (n -VectSp_over K) & the_rank_of (1. (K,n)) = n )
set ONE = 1. (K,n);
( n = 0 or n >= 1 ) by NAT_1:14;
then A1: Det (1. (K,n)) = 1_ K by MATRIXR2:41, MATRIX_7:16;
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 A2: 1. (K,n) is diagonal by MATRIX_1:def 6;
1_ K <> 0. K ;
then the_rank_of (1. (K,n)) = n by A1, Th83;
hence ( lines (1. (K,n)) is Basis of (n -VectSp_over K) & the_rank_of (1. (K,n)) = n ) by A2, Th111; :: thesis: verum