let a be Element of 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) )
reconsider aa = a as Element of F_Real by VECTSP_1:def 15;
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 15;
hence (a * M) * i,j = a * (M * i,j) by VECTSP_1:def 15; :: thesis: verum