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