let i, j be Element of 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