let a be real number ; :: thesis: for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds
a * (A + B) = (a * A) + (a * B)
let A, B be Matrix of REAL ; :: thesis: ( len A = len B & width A = width B & len A > 0 implies a * (A + B) = (a * A) + (a * B) )
assume A1: ( len A = len B & width A = width B & len A > 0 ) ; :: thesis: a * (A + B) = (a * A) + (a * B)
reconsider ea = a as Element of F_Real by XREAL_0:def 1;
A2: a * (A + B) = MXF2MXR (ea * (MXR2MXF (A + B))) by Def7
.= MXF2MXR ((ea * (MXR2MXF A)) + (ea * (MXR2MXF B))) by A1, MATRIX_5:36 ;
(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))) ;
hence a * (A + B) = (a * A) + (a * B) by A2; :: thesis: verum