let A be Matrix of REAL ; :: thesis: for i, j being Element of NAT st [i,j] in Indices A holds
(- A) * i,j = - (A * i,j)
let i, j be Element of 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