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

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