let i, j be Nat; for M being Matrix of REAL st [i,j] in Indices M holds
(- M) * (i,j) = - (M * (i,j))
let M be Matrix of REAL; ( [i,j] in Indices M implies (- M) * (i,j) = - (M * (i,j)) )
assume
[i,j] in Indices M
; (- M) * (i,j) = - (M * (i,j))
then
(- M) * (i,j) = - ((MXR2MXF M) * (i,j))
by MATRIX_3:def 2, VECTSP_1:def 5;
hence
(- M) * (i,j) = - (M * (i,j))
by VECTSP_1:def 5; verum