let M be Matrix of COMPLEX; :: thesis: (- 1) * M = - M
A1: width (- M) = width M by Th8;
A2: width ((- 1) * M) = width M by Th2;
A3: len ((- 1) * M) = len M by Th2;

A4: now :: thesis: for i, j being Nat st [i,j] in Indices ((- 1) * M) holds
((- 1) * M) * (i,j) = (- M) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices ((- 1) * M) implies ((- 1) * M) * (i,j) = (- M) * (i,j) )
assume A5: [i,j] in Indices ((- 1) * M) ; :: thesis: ((- 1) * M) * (i,j) = (- M) * (i,j)
then A6: 1 <= i by Th1;
A7: 1 <= j by A5, Th1;
A8: j <= width M by A2, A5, Th1;
i <= len M by A3, A5, Th1;
then A9: [i,j] in Indices M by A6, A7, A8, Th1;
hence ((- 1) * M) * (i,j) = (- 1) * (M * (i,j)) by Th3
.= - (M * (i,j))
.= (- M) * (i,j) by A9, Th9 ;
:: thesis: verum

end;

len (- M) = len M by Th8;
hence (- 1) * M = - M by A3, A1, A2, A4, MATRIX_0:21; :: thesis: verum