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

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

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

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

then (- M) * (i,j) = - ((MXR2MXF M) * (i,j)) by MATRIX_3:def 2, VECTSP_1:def 5;

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

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

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

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

then (- M) * (i,j) = - ((MXR2MXF M) * (i,j)) by MATRIX_3:def 2, VECTSP_1:def 5;

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