let a be Real; :: thesis: for A, B being Matrix of REAL st width A = len B holds
A * (a * B) = a * (A * B)
let A, B be Matrix of REAL; :: thesis: ( width A = len B implies A * (a * B) = a * (A * B) )
assume A1: width A = len B ; :: thesis: A * (a * B) = a * (A * B)
reconsider ea = a as Element of F_Real by XREAL_0:def 1;
thus A * (a * B) = MXF2MXR ((MXR2MXF A) * (MXR2MXF (MXF2MXR (ea * (MXR2MXF B))))) by Def7
.= MXF2MXR (ea * (MXR2MXF (MXF2MXR ((MXR2MXF A) * (MXR2MXF B))))) by A1, Th22
.= a * (A * B) by Def7 ; :: thesis: verum