for n being Nat
for K being Field
for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)