let K be Field; :: thesis: for n being Nat
for M1 being Matrix of n,K holds (- M1) @ = - (M1 @ )
let n be Nat; :: thesis: for M1 being Matrix of n,K holds (- M1) @ = - (M1 @ )
let M1 be Matrix of n,K; :: thesis: (- M1) @ = - (M1 @ )
for i, j being Nat st [i,j] in Indices ((- M1) @ ) holds
((- M1) @ ) * i,j = (- (M1 @ )) * i,j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((- M1) @ ) implies ((- M1) @ ) * i,j = (- (M1 @ )) * i,j )
assume A1: [i,j] in Indices ((- M1) @ ) ; :: thesis: ((- M1) @ ) * i,j = (- (M1 @ )) * i,j
then [i,j] in [:(Seg n),(Seg n):] by MATRIX_1:25;
then ( i in Seg n & j in Seg n ) by ZFMISC_1:106;
then [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:106;
then A2: ( [j,i] in Indices M1 & [j,i] in Indices (- M1) ) by MATRIX_1:25;
A3: [i,j] in Indices (M1 @ ) by A1, MATRIX_1:27;
((- M1) @ ) * i,j = (- M1) * j,i by A2, MATRIX_1:def 7
.= - (M1 * j,i) by A2, MATRIX_3:def 2
.= - ((M1 @ ) * i,j) by A2, MATRIX_1:def 7
.= (- (M1 @ )) * i,j by A3, MATRIX_3:def 2 ;
hence ((- M1) @ ) * i,j = (- (M1 @ )) * i,j ; :: thesis: verum

end;

hence (- M1) @ = - (M1 @ ) by MATRIX_1:28; :: thesis: verum