theorem :: MATRIX11:62

for n being Nat
for K being commutative Ring st not K is degenerated & K is well-unital & K is domRing-like holds
for A, B being Matrix of n,K st 0 < n holds
Det (A * B) = (Det A) * (Det B)