let A be Matrix of REAL; :: thesis: for i, j being Nat st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
let i, j be Nat; :: thesis: ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) )
assume A1: [i,j] in Indices A ; :: thesis: (- A) * (i,j) = - (A * (i,j))
- A = (- 1) * A by Th9;
then (- A) * (i,j) = (- 1) * (A * (i,j)) by A1, MATRIXR1:29;
hence (- A) * (i,j) = - (A * (i,j)) ; :: thesis: verum