let n be Nat; :: thesis: for K being Field
for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)
let K be Field; :: 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;