for n being Nat
for K being Field
for R being FinSequence_of_Square-Matrix of K holds Det (R | n) = (Det R) | n