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

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