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

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