for n being Nat st n > 0 holds
Det (0_Rmatrix n) = 0