let n be Nat; :: thesis: for K being Field holds the_rank_of (1. (K,n)) = n
let K be Field; :: thesis: the_rank_of (1. (K,n)) = n
A1: 1_ K <> 0. K ;
( n + 0 > 0 or n = 0 ) ;
then A2: ( n >= 1 or n = 0 ) by NAT_1:19;
Det (1. (K,n)) = 1_ K by A2, MATRIXR2:41, MATRIX_7:16;
hence the_rank_of (1. (K,n)) = n by A1, MATRIX13:83; :: thesis: verum