theorem :: MATRIX11:62

for n being Nat
for K being commutative Ring
for A, B being Matrix of n,K st 0 < n holds
Det (A * B) = (Det A) * (Det B)