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