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