let a be Element of REAL ; :: thesis: for i, j being Nat
for M being Matrix of REAL st len (a * M) = len M & width (a * M) = width M & [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 len (a * M) = len M & width (a * M) = width M & [i,j] in Indices M holds
(a * M) * i,j = a * (M * i,j)
let M be Matrix of REAL ; :: thesis: ( len (a * M) = len M & width (a * M) = width M & [i,j] in Indices M implies (a * M) * i,j = a * (M * i,j) )
assume A1: ( len (a * M) = len M & width (a * M) = width M & [i,j] in Indices M ) ; :: thesis: (a * M) * i,j = a * (M * i,j)
reconsider aa = a as Element of F_Real by VECTSP_1:def 15;
MXR2MXF (a * M) = MXR2MXF (MXF2MXR (aa * (MXR2MXF M))) by MATRIXR1:def 7
.= aa * (MXR2MXF M) ;
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