let i, j be Nat; :: thesis: for A being Matrix of REAL st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
let A be Matrix of REAL; :: thesis: ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) )
assume [i,j] in Indices A ; :: thesis: (- A) * (i,j) = - (A * (i,j))
then (- A) * (i,j) = - ((MXR2MXF A) * (i,j)) by MATRIX_3:def 2;
hence (- A) * (i,j) = - (A * (i,j)) ; :: thesis: verum