let n be Nat; :: thesis: Det (1_Rmatrix n) = 1

per cases ( n >= 1 or n < 1 ) ;

suppose n >= 1 ; :: thesis: Det (1_Rmatrix n) = 1

hence Det (1_Rmatrix n) = 1_ F_Real by MATRIX_7:16
.= 1 ;
:: thesis: verum

end;

suppose n < 1 ; :: thesis: Det (1_Rmatrix n) = 1

then n = 0 by NAT_1:25;
hence Det (1_Rmatrix n) = 1. F_Real by Th41
.= 1 ;
:: thesis: verum

end;

end;