let i, j be Element of NAT ; :: thesis: for A being Matrix of REAL st len (- A) = len A & width (- A) = width A & [i,j] in Indices A holds
(- A) * i,j = - (A * i,j)
let A be Matrix of REAL ; :: thesis: ( len (- A) = len A & width (- A) = width A & [i,j] in Indices A implies (- A) * i,j = - (A * i,j) )
assume A1: ( len (- A) = len A & width (- A) = width A & [i,j] in Indices A ) ; :: thesis: (- A) * i,j = - (A * i,j)
(- A) * i,j = - ((MXR2MXF A) * i,j) by A1, MATRIX_3:def 2;
hence (- A) * i,j = - (A * i,j) ; :: thesis: verum