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 15;
hence (- M) * i,j = - (M * i,j) by VECTSP_1:def 15; :: thesis: verum