let n be Nat; :: thesis: ( n > 0 implies Det (0_Rmatrix n) = 0 )
set K = F_Real ;
assume n > 0 ; :: thesis: Det (0_Rmatrix n) = 0
then n >= 0 + 1 by NAT_1:13;
then Det (0_Rmatrix n) = 0. F_Real by MATRIX_7:15
.= 0 ;
hence Det (0_Rmatrix n) = 0 ; :: thesis: verum