let n be Nat; :: thesis: for A, B being Matrix of n,REAL holds MXR2MXF (A * B) = (MXR2MXF A) * (MXR2MXF B)
let A, B be Matrix of n,REAL; :: thesis: MXR2MXF (A * B) = (MXR2MXF A) * (MXR2MXF B)
A * B = (MXF2MXR (MXR2MXF A)) * B by Lm06
.= (MXF2MXR (MXR2MXF A)) * (MXF2MXR (MXR2MXF B)) by Lm06
.= MXF2MXR ((MXR2MXF A) * (MXR2MXF B)) by Lm05 ;
hence MXR2MXF (A * B) = (MXR2MXF A) * (MXR2MXF B) by ANPROJ_8:16; :: thesis: verum