let n be Nat; :: thesis: for A, B being Matrix of n,F_Real holds MXF2MXR (A * B) = (MXF2MXR A) * (MXF2MXR B)
let A, B be Matrix of n,F_Real; :: thesis: MXF2MXR (A * B) = (MXF2MXR A) * (MXF2MXR B)
(MXF2MXR A) * (MXF2MXR B) = MXF2MXR ((MXR2MXF (MXF2MXR A)) * (MXR2MXF (MXF2MXR B))) by MATRIXR1:def 6
.= MXF2MXR (A * (MXR2MXF (MXF2MXR B))) by ANPROJ_8:16
.= MXF2MXR (A * B) by ANPROJ_8:16 ;
hence MXF2MXR (A * B) = (MXF2MXR A) * (MXF2MXR B) ; :: thesis: verum