let a be Real; :: thesis: for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 holds
A * (a * B) = a * (A * B)
let A, B be Matrix of REAL ; :: thesis: ( width A = len B & len A > 0 & len B > 0 implies A * (a * B) = a * (A * B) )
assume A1: ( width A = len B & len A > 0 & len B > 0 ) ; :: thesis: A * (a * B) = a * (A * B)
reconsider ea = a as Element of F_Real ;
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