let n be Nat; :: thesis: for K being commutative Ring
for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)
let K be commutative Ring; :: thesis: for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)
let A, B be Matrix of n,K; :: thesis: Det (A * B) = (Det A) * (Det B)

per cases ( n > 0 or n <= 0 ) ;

suppose n > 0 ; :: thesis: Det (A * B) = (Det A) * (Det B)

hence Det (A * B) = (Det A) * (Det B) by MATRIX11:62; :: thesis: verum

end;

suppose n <= 0 ; :: thesis: Det (A * B) = (Det A) * (Det B)

then A1: n = 0 ;
hence Det (A * B) = 1. K by Th41
.= (1. K) * (1. K)
.= (Det A) * (1. K) by A1, Th41
.= (Det A) * (Det B) by A1, Th41 ;
:: thesis: verum

end;

end;