let K be Field; :: thesis: for A being Matrix of K holds Indices A = Indices (- A)
let A be Matrix of K; :: thesis: Indices A = Indices (- A)
dom A = Seg (len A) by FINSEQ_1:def 3
.= Seg (len (- A)) by MATRIX_3:def 2
.= dom (- A) by FINSEQ_1:def 3 ;
hence Indices A = Indices (- A) by MATRIX_3:def 2; :: thesis: verum