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;
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 A1: 1. K,n is diagonal by MATRIX_1:def 15;
( ( n = 0 or n >= 1 ) & n in NAT ) by NAT_1:14, ORDINAL1:def 13;
then ( Det (1. K,n) = 1_ K & 1_ K <> 0. K ) by MATRIXR2:41, MATRIX_7:16;
then the_rank_of (1. K,n) = n by Th83;
hence ( lines (1. K,n) is Basis of n -VectSp_over K & the_rank_of (1. K,n) = n ) by A1, Th111; :: thesis: verum