let n be Nat; :: thesis: for A, B being Matrix of n,REAL holds Det (A * B) = (Det A) * (Det B)
set K = F_Real ;
let A, B be Matrix of n,REAL; :: thesis: Det (A * B) = (Det A) * (Det B)
reconsider Na = MXR2MXF A, Nb = MXR2MXF B as Matrix of n,F_Real ;
Det (A * B) = (Det Na) * (Det Nb) by Th45
.= (Det A) * (Det B) ;
hence Det (A * B) = (Det A) * (Det B) ; :: thesis: verum