let A be Matrix of REAL; for i, j being Nat st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
let i, j be Nat; ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) )
assume A1:
[i,j] in Indices A
; (- 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))
; verum