let i, j be Nat; 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; ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) )
assume
[i,j] in Indices A
; (- 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))
; verum