let a be Real; :: thesis: for i, j being Nat

for M being Matrix of REAL st [i,j] in Indices M holds

(a * M) * (i,j) = a * (M * (i,j))

let i, j be Nat; :: thesis: for M being Matrix of REAL st [i,j] in Indices M holds

(a * M) * (i,j) = a * (M * (i,j))

let M be Matrix of REAL; :: thesis: ( [i,j] in Indices M implies (a * M) * (i,j) = a * (M * (i,j)) )

a in REAL by XREAL_0:def 1;

then reconsider aa = a as Element of F_Real by VECTSP_1:def 5;

A1: MXR2MXF (a * M) = MXR2MXF (MXF2MXR (aa * (MXR2MXF M))) by MATRIXR1:def 7

.= aa * (MXR2MXF M) ;

assume [i,j] in Indices M ; :: thesis: (a * M) * (i,j) = a * (M * (i,j))

then (a * M) * (i,j) = aa * ((MXR2MXF M) * (i,j)) by A1, MATRIX_3:def 5, VECTSP_1:def 5;

hence (a * M) * (i,j) = a * (M * (i,j)) by VECTSP_1:def 5; :: thesis: verum

for M being Matrix of REAL st [i,j] in Indices M holds

(a * M) * (i,j) = a * (M * (i,j))

let i, j be Nat; :: thesis: for M being Matrix of REAL st [i,j] in Indices M holds

(a * M) * (i,j) = a * (M * (i,j))

let M be Matrix of REAL; :: thesis: ( [i,j] in Indices M implies (a * M) * (i,j) = a * (M * (i,j)) )

a in REAL by XREAL_0:def 1;

then reconsider aa = a as Element of F_Real by VECTSP_1:def 5;

A1: MXR2MXF (a * M) = MXR2MXF (MXF2MXR (aa * (MXR2MXF M))) by MATRIXR1:def 7

.= aa * (MXR2MXF M) ;

assume [i,j] in Indices M ; :: thesis: (a * M) * (i,j) = a * (M * (i,j))

then (a * M) * (i,j) = aa * ((MXR2MXF M) * (i,j)) by A1, MATRIX_3:def 5, VECTSP_1:def 5;

hence (a * M) * (i,j) = a * (M * (i,j)) by VECTSP_1:def 5; :: thesis: verum