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